А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?
появление теории типов было обусловлено тем, что теория множеств приводила к парадоксам
Это было самым-самым началом. Потом теорию множеств пофиксили и сейчас в ZFC нет парадоксов
что обесценивает эту проверку.
Я бы не сказал, что обесценивает. Но тут надо уточнить, что вы имеете в виду под неконструктивной математикой? Вы не признаете аксиому исключения третьего, или шире понимаете неконструктивность?
блин проще не задумываясь, в потоке, написать всё в одном классе
Так делать точно не нужно. Это будет страшный спагетти-код. Помимо простого деления на бизнес логику и работу с вводом\выводом, есть еще и другие слои, например работу с БД принято выносить в DAO-классы. Интеграции с внешними системами - тоже в отдельные классы и отдельные пакеты. Иногда даже в отдельные библиотеки. А еще, принято использовать паттерны проектирования, и они, как правило, тоже выносятся в отдельные классы
Почему не очень? Вроде неплохо получилось, технически все сходится и выводится. Иногда очень долго и не всегда красиво, но все равно оно работает и адекватной замены аксиоматической теории множеств я пока не вижу. Ну разве что, coq вроде неплохо через индуктивные типы многие штуки представляет.
зачем заморачиваться с неконструктивной математикой, если априори известно, что это бесполезный математический онанизм?
А все классические учебники по анализу\теории вероятности, они же сильно неконструктивные, там каждая третья теорема использует аксиому исключения среднего в явной или неявной форме. Если только конструктивный подход использовать, есть учебник по конструктивной теории множеств и конструктивному анализу, но мне они показались весьма экспериментальными...
На стажера спрашивают совсем-совсем простые алгоритмы вроде цикла for по массиву.
Ваше сообщение составлено без опыта собеседований и понимания реальной ситуации на рынке, а также без знаний ситуации с алгоритмическими собеседованиями. Например, в некоторые команды Яндекса принимают по сокращенной программе собеседований, в которой только 2 технических (алгоритмических) собеседования. По личному опыту, я проходил в команду Яндекс.Медиасервисы в 2021 году на 17-й грейд (это эквивалент Синьера). И там не было чего-то особо сложного, среднего уровня типовые задачи.
Ну это очень мутное понятие, каждый его по-разному интерпретирует. Как вы формально определите критерии "хорошего программиста"?
Для некоторых хороший программист - это тот, кто просто умеет писать чистый код. Для других - тот, кто умеет нужные библиотеки и фреймворки подключать\соединять. Для третьих это тот, кто удобен бизнесу и понимает требования\решает проблемы в адекватный срок. Для четвертых это тот, кто хорошо знает алгоритмы и структуры данных, сердце компьютерных наук.
Все это я уже проходил и хочется двигаться дальше.
ничуть не помешает изучению, зато позволит [вашим конкурентам] начать его раньше.
Да у нас вроде нету спешки проходить настолько базовые предметы. Они же проходятся один раз и на всю жизнь, и лучше это сделать более качественно и глубоко (на мой взгляд). Еще можно разбить на 2 этапа, в первом этапе вы проходите эти предметы по какому-нибудь поверхностному курсу, а потом возвращаетесь и проходите по более глубокому курсу с более глубоким покрытием фундамента. Собственно, я пошел именно таким путем почти по всем предметам.
Вы же сдавали философию...
Так вот, как раз философия и заставляет двигаться глубже. В общих чертах этот пункт я понимаю уже давно, уровни организации материи всякие (стандартная модель -> физика -> химия -> биология -> астрофизика -> теория большого взрыва). Но хочется больше деталей и формальной верификации, так как очень много дыр в понимании.
Кстати большинство (и я в том числе) проголосовали за постижение Тайн Мироздания:)
Вот тут для меня была неожиданность, действительно этот пункт оказался очень популярен и сейчас лидирует. Мне тоже интересно =) Но ML в большем приоритете у меня
Увы, в моем ВУЗе все эти основания математики не изучали
А у кого их изучали?) Ладно, у нас был профессор Лагодинский, который давал математическую логику довольно глубоко. Но не конструктивным путем (через таблицы истинности) и без опоры на формализацию и теорем-пруверы.
что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
у вас геометрическая/топологическая интуиция прокачана
Ох не люблю я эту геометрическую интуицию, всегда ее ненавидел еще со школы... Бррррр
Спасибо за замечание, мб прочитать первые пару-тройку глав действительно стоит, прочтение книги занимает в 4-5 раз меньше усилий, чем прочтение + выполнение упражнений + их формализация
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения,
Плюсую, языки программирования именно этим путем развиваются. C++ -> Java -> Kotlin все больше и больше проверяют на этапе компиляции. Дошло до того, что Kotlin банально заставляет вас прорабатывать все null-типы через if, чтобы потом на проде не словить NPE
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Про ETCS интересно, спасибо.
Я бы не стал, получится неудобная и неизящная конструкция.
А как мы ее тогда в теорем-прувере формализовать будем?
Спасибо за интересное обсуждение. Про мир реальных приложений (запрос к веб-приложению и микросервисы) - это как раз то, чем я профессионально занимаюсь на основной работе как Java-разработчик уже много-много лет. Хочу вам сказать, что строгая типизация для высоконагруженных бэкенд-приложений просто жизненного необходима, она очень много ошибок предотвращает. Например, мы на работе очень часто задаем, что запрос пользователя должен быть строго по спецификации (ООП иерархия объектов) и некоторые поля обязательно должны присутствовать, другие должны иметь минимальную длину и так далее. Например, аннотации javax.validation используются.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Да из личного опыта программирования этой теории типов - 11 правил выведения типов довольно легко запрограммировать. А вот если вы теорию множеств захотите запрограммировать - все не так просто, там придется теорию типов вводить\придумывать к ней.
Посмотрел. Да, перевод есть, но он 7-ми летней давности (книга много обновлялась) и не все главы переведены, например IndPrinciples.v только заголовки переведены. Впрочем, это не проблема - можно скормить эти исходники какому-нибудь переводчику и он должен легко справиться с переводом, так как исходники книги - доступны
Может тут имеется в виду чистое программирование в любом виде или решение алгоритмических задач?
Интересно, зачем им Coq, они же "EX CORP. Мы создаем экосистему сервисов для игроков соревновательных игр"
Про аксиому выбора - да, все верно, она неконструктивна
А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?
Это было самым-самым началом. Потом теорию множеств пофиксили и сейчас в ZFC нет парадоксов
Я бы не сказал, что обесценивает. Но тут надо уточнить, что вы имеете в виду под неконструктивной математикой? Вы не признаете аксиому исключения третьего, или шире понимаете неконструктивность?
Так делать точно не нужно. Это будет страшный спагетти-код. Помимо простого деления на бизнес логику и работу с вводом\выводом, есть еще и другие слои, например работу с БД принято выносить в DAO-классы. Интеграции с внешними системами - тоже в отдельные классы и отдельные пакеты. Иногда даже в отдельные библиотеки. А еще, принято использовать паттерны проектирования, и они, как правило, тоже выносятся в отдельные классы
Почему не очень? Вроде неплохо получилось, технически все сходится и выводится. Иногда очень долго и не всегда красиво, но все равно оно работает и адекватной замены аксиоматической теории множеств я пока не вижу. Ну разве что, coq вроде неплохо через индуктивные типы многие штуки представляет.
А все классические учебники по анализу\теории вероятности, они же сильно неконструктивные, там каждая третья теорема использует аксиому исключения среднего в явной или неявной форме. Если только конструктивный подход использовать, есть учебник по конструктивной теории множеств и конструктивному анализу, но мне они показались весьма экспериментальными...
На стажера спрашивают совсем-совсем простые алгоритмы вроде цикла for по массиву.
Ваше сообщение составлено без опыта собеседований и понимания реальной ситуации на рынке, а также без знаний ситуации с алгоритмическими собеседованиями. Например, в некоторые команды Яндекса принимают по сокращенной программе собеседований, в которой только 2 технических (алгоритмических) собеседования. По личному опыту, я проходил в команду Яндекс.Медиасервисы в 2021 году на 17-й грейд (это эквивалент Синьера). И там не было чего-то особо сложного, среднего уровня типовые задачи.
Ну это очень мутное понятие, каждый его по-разному интерпретирует. Как вы формально определите критерии "хорошего программиста"?
Для некоторых хороший программист - это тот, кто просто умеет писать чистый код. Для других - тот, кто умеет нужные библиотеки и фреймворки подключать\соединять. Для третьих это тот, кто удобен бизнесу и понимает требования\решает проблемы в адекватный срок. Для четвертых это тот, кто хорошо знает алгоритмы и структуры данных, сердце компьютерных наук.
Все это я уже проходил и хочется двигаться дальше.
Да у нас вроде нету спешки проходить настолько базовые предметы. Они же проходятся один раз и на всю жизнь, и лучше это сделать более качественно и глубоко (на мой взгляд). Еще можно разбить на 2 этапа, в первом этапе вы проходите эти предметы по какому-нибудь поверхностному курсу, а потом возвращаетесь и проходите по более глубокому курсу с более глубоким покрытием фундамента. Собственно, я пошел именно таким путем почти по всем предметам.
Так вот, как раз философия и заставляет двигаться глубже. В общих чертах этот пункт я понимаю уже давно, уровни организации материи всякие (стандартная модель -> физика -> химия -> биология -> астрофизика -> теория большого взрыва). Но хочется больше деталей и формальной верификации, так как очень много дыр в понимании.
Вот тут для меня была неожиданность, действительно этот пункт оказался очень популярен и сейчас лидирует. Мне тоже интересно =) Но ML в большем приоритете у меня
А у кого их изучали?) Ладно, у нас был профессор Лагодинский, который давал математическую логику довольно глубоко. Но не конструктивным путем (через таблицы истинности) и без опоры на формализацию и теорем-пруверы.
Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
Ох не люблю я эту геометрическую интуицию, всегда ее ненавидел еще со школы... Бррррр
Спасибо за замечание, мб прочитать первые пару-тройку глав действительно стоит, прочтение книги занимает в 4-5 раз меньше усилий, чем прочтение + выполнение упражнений + их формализация
Плюсую, языки программирования именно этим путем развиваются. C++ -> Java -> Kotlin все больше и больше проверяют на этапе компиляции. Дошло до того, что Kotlin банально заставляет вас прорабатывать все null-типы через if, чтобы потом на проде не словить NPE
Бешено плюсую
Под чит-опцией я как раз и имел в виду ту опцию, что делает Set импредикативным
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Про ETCS интересно, спасибо.
А как мы ее тогда в теорем-прувере формализовать будем?
Слышал про seL4, крутая штука. У coq правда есть аналогичный проект - CertiKOS
Интересно, спасибо. У Coq есть такая проблема, что на нем самом не очень получится приложения разработать
Спасибо за интересное обсуждение. Про мир реальных приложений (запрос к веб-приложению и микросервисы) - это как раз то, чем я профессионально занимаюсь на основной работе как Java-разработчик уже много-много лет. Хочу вам сказать, что строгая типизация для высоконагруженных бэкенд-приложений просто жизненного необходима, она очень много ошибок предотвращает. Например, мы на работе очень часто задаем, что запрос пользователя должен быть строго по спецификации (ООП иерархия объектов) и некоторые поля обязательно должны присутствовать, другие должны иметь минимальную длину и так далее. Например, аннотации javax.validation используются.
Да из личного опыта программирования этой теории типов - 11 правил выведения типов довольно легко запрограммировать. А вот если вы теорию множеств захотите запрограммировать - все не так просто, там придется теорию типов вводить\придумывать к ней.
Посмотрел. Да, перевод есть, но он 7-ми летней давности (книга много обновлялась) и не все главы переведены, например IndPrinciples.v только заголовки переведены. Впрочем, это не проблема - можно скормить эти исходники какому-нибудь переводчику и он должен легко справиться с переводом, так как исходники книги - доступны
Да я согласен, что нужно. Конечно может -)