У нас есть 3 «теории всего» — научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики представляет особый интерес, так как он является фундаментом для двух других фундаментов и имеет глубокий философский смысл. Последние 2 года (2023–2024) я сильно им увлекся и проделал довольно большую работу по углубленному изучению теории типов (Calculus of Constructions), и готов поделиться результатами, а также рассказать о девяти направлениях, где можно применить это на практике. Очень многое получилось лучше, чем я планировал. Изначально перспективы были не очень понятными, и поэтому я не рассказывал друзьям и коллегам про мою работу в этом направлении и называл это «Секретный Проект». Но теперь, когда многое прояснилось и получилось, можно поделиться успехом. Собственно, в этой статье я расскажу вам не только про сам фундамент математики, а еще его связь с ежедневной работой программиста, а также с Computer Science/Data Science и AI/ML. Я вам нарисую большую и красивую картину, на которой все понятно и логически следует из маленького набора правил выведений типов (11 штук) и аксиом теории множеств (9 штук).
У нас есть 3 фундамента математики — теория множеств (удобна для человека), теория типов (удобна для компьютера) и теория категорий (не знаю, зачем она вообще нужна). Они примерно одинаковой мощности и одну можно выразить внутри другой. Особый интерес представляет именно теория типов, т.к. ее довольно легко можно запрограммировать внутри компьютера и использовать как строгий фундамент для других теорий, который не дает совершить ошибку и проверяет каждое ваше действие.
А сейчас я вам расскажу короткую историю теорем‑пруверов (пруф‑ассистентов) — это такие программы, которые позволяют доказывать математические теоремы и строить на их основе фундамент математики с нуля. В 1973 появился проект Mizar (в Польше) и он был первым успешным теорем‑прувером. На данный момент его библиотека — самая большая (52,000 доказанных теорем и 10,000 математических определений).
Разработчики Mizar попробовали создать теорем‑прувер полностью на теории множеств (что казалось логичным на тот момент), но в итоге получился огромный архитектурный костыль — им пришлось поддерживать 2 ядра одновременно (теория типов и теория множеств) вместо одного. Это плохо не только для разработки/поддержки системы, но и для освоения\обучения\расширения.
Прошло время и теория типов сформировалась как отдельная дисциплина, хорошо проработанная и сформированная. Исследователям удалось очень чисто (без костылей) выразить математическую логику внутри теории типов, и сделать ее 100% совместимой с тем, как думают математики. Как им удалось до этого догадаться и сделать такой большой прорыв — я не знаю. Так вот, если мы полностью формализуем математическую логику, то аксиоматическая теория множеств очень чисто и легко выводится из нее. Нужно всего лишь аксиоматически задать существование отношения принадлежности к множеству (∈), а также добавить 9 аксиом ZFC (Zermelo‑Fraenkel Set Theory), которые по сути постулируют существование двух множеств (пустое и бесконечное) и как с ними работать. А саму формальную систему математической логики (набор правил) называют Натуральная Дедукция.
Есть 2 популярные теории типов — Martin‑Löf type theory (MLTT) и Calculus of Construction (CoC). Они примерно одинаковой мощности и имеют скорее культурную\территориальную разницу. Тем не менее, Calculus of Construction немного новее и компактнее, а также используется двумя самыми популярными в индустрии теорем‑пруверами — Coq и Lean. А еще по ней есть супер‑качественный и новый учебник от Роба Недерпелта (Type Theory and Formal Proof: An Introduction). Поэтому я выбрал именно ее.
Собственно, 80% моих усилий по изучению фундамента математики на протяжении последних двух лет построены вокруг этой офигенной книги. Авторы книги проделали огромную работу и проанализировали 147 источников (другие книги и статьи), чтобы собрать все самое лучшее в одном месте. Благодаря их труду, я освоил эту область всего за 2 года вместо 10 лет. Я прорешал почти всю книгу и почти все упражнения, полностью покрыв первые 13 глав (300 страниц) книги. Эта книга строит фундамент математики с полного нуля и объясняет\формально вводит вообще все концепции и нотации. Одна из интересных особенностей книги в том, что автор использует современный конструктивный подход и выражает математическую логику полностью конструктивным способом, не использовав таблицу истинности ни разу. Это очень хорошо для обучения и понимания, а также наглядно показывает, как теория типов может переплетаться с математической логикой и чем на самом деле являются многие логические операции на низком уровне.
Можно разбить содержимое книги на 3 части — в первой части (1 — 6 главы) автор с полного нуля (с лямбда‑исчисления) постепенно достраивает и усложняет систему типов и проходится по всему лямбда‑кубу, чтобы получить в итоге золотую классику — Calculus of Constructions (λC). Во второй части (7 — 13 главы) — автор рассказывает, как запихнуть в эту теорию типов математическую логику и теорию множеств. В третьей части (14 — 15 главы) автор формализует целые числа (Z) и их арифметику внутри теории типов, дает основы теории чисел, а также формализует доказательство теоремы Безу в качестве демонстрации работы системы типов.
Собственно, главы 1–7 я прорешал на бумаге (со 100%‑м покрытием всех упражнений в конце глав), потом я написал маленькое мобильное приложение под андроид (MathConstructor) и в нем покрыл главы 5,6,7 и 11. Главы 11–13 я покрыл уже внутри Coq, исходники можете найти в моем GitHub. И это получилось очень круто и полезно и эффективно! А на 14–15 главы у меня не хватило мотивации, т.к. в 13-й главе автор не очень чисто покрыл теорию множеств. Он решил использовать гибридный подход (с костылями внедрить многие концепции теории множеств в теорию типов, вместо того, чтобы чисто выводить все из аксиом ZFC). Мне это совсем не понравилось и пришлось переключиться на другой учебник по теории множеств.
Главы книги, их покрытие, оценка сложности и инструменты, которые я использовал для обучения
|
№ |
Глава |
Сложность |
Мое покрытие |
Я использовал |
Рекомендую вам |
1 |
Untyped lambda calculus |
9 |
100% |
Pen & Paper, Anki |
Pen & Paper, Anki |
2 |
Simply typed lambda calculus |
6 |
100% |
Pen & Paper, Anki |
Coq |
3 |
Second order typed lambda calculus |
5 |
100% |
Pen & Paper, Anki |
Coq |
4 |
Types dependent on types |
5 |
100% |
Pen & Paper, Anki, Custom App |
Coq |
5 |
Types dependent on terms |
5 |
100% |
Pen & Paper, Anki, Custom App |
Coq |
6 |
The Calculus of Constructions |
5 |
100% |
Pen & Paper, Anki, Custom App |
Coq |
7 |
The encoding of logical notions in λC |
7 |
100% |
Custom App |
Coq |
8 |
Definitions |
4 |
100% |
Pen & Paper |
Coq |
9 |
Extension of λC with definitions |
5 |
100% |
Pen & Paper |
Coq |
10 |
Rules and properties of λD |
5 |
100% |
Pen & Paper |
Coq |
11 |
Flag‑style natural deduction in λD |
7 |
100% |
Custom App, Coq |
Coq |
12 |
Mathematics in λD: a first attempt |
6 |
100% |
Coq |
Coq |
13 |
Sets and subsets |
7 |
100% |
Coq |
- |
14 |
Numbers and arithmetic in λD |
8 |
0% |
- |
- |
15 |
An elaborated example |
7 |
0% |
- |
- |
16 |
Further perspectives |
3 |
100% |
- |
- |
Собтсвенно, после 13й главы я рекомендую вам переключиться на книгу по теории множеств
Собственно, я взял старый и классический учебник по теории множеств от 1963 года (Set theory and logic by Robert Stoll), и сразу прыгнул на 7 главу (Informal Axiomatic Set Theory), которая дает аксиомы ZFC и выводит из них множество натуральных чисел и его базовые свойства, и формализовал примерно половину главы за месяц. Это была проверка теории типов и Coq на прочность — и проверка успешно пройдена! Я был поражен тем, насколько автор 1963 года все четко излагает. Даже самые странные его утверждения и математические конструкции оказались очень нужны и полезны при формализации. Все его шаги, 100% ход мыслей можно 1–1 перенести на формальный язык теории типов. В общем, мне опять повезло с книгой, хоть там и много технических опечаток, но они — не проблема. Я точно уверен, что вернусь к этой книге еще.
В итоге, мне всего за месяц удалось закрыть огромное количество «серых зон» и пробелов в понимании ключевых математических концепций, которые у меня образовались в 2021 — 2022 году по мере прохождения различных стандартных математических курсов типа Calculus I / II / III. Мне удалось доказать существование множества натуральных чисел (N) — вытащить его из аксиомы бесконечности (ZF_Infinity), а также вывести 5 аксиом Пиано (на них все числовые системы строятся), а еще вывести принцип математической индукции, а из него — вывести принцип сильной индукции. Еще мне удалось из общей аксиомы выбора (ZF7_Choice) вывести частную аксиому выбора (более удобную), а из нее (используя теорему Диаконеску) вывести аксиому исключения среднего (excluding third), на которой базируется вся неконструктивная (классическая) математика. И все это очень интересно и полезно. Многие аксиомы для меня больше не являются аксиомами, а выводятся из 9 аксиом ZFC. Мне очень нравиться такой подход. Возможно, мне близка философия логистов и формалистов.
В итоге, на основе этих двух книг по теории типов и теории множеств, мне удалось заложить основы собственной библиотеки Coq, которая написана полностью с нуля и которую я понимаю на 100% как она работает изнутри. Я долго думал, как ее назвать, и ChatGPT предложил мне название ZFCFramework. Так и назовем ее. Собственно, в ближайшие пару лет я планирую ее активно развивать и наращивать, применять для разных обучающих целей. Очень круто, что у меня теперь есть такой инструмент. Если я буду погружаться в разные разделы математики и проходить новые курсы, я могу параллельно формализовать их в Coq и усиливать фундамент, а также получать максимальный выхлоп и максимально глубокий результат от потраченных сил на курсы или учебники.
По поводу моего мобильного Android‑приложения MathConstructor: я пока его нигде не выкладывал, но планирую выложить где‑нибудь в 2025 году вместе со всеми исходниками, и под это будет отдельная статья. Но вам не обязательно ждать — вы можете разработать свой аналог — и это совсем не трудно! На разработку рабочей Calculus of Constructions мне понадобилось всего 4 дня, и главы 5–6–7 уже почти полностью покрывались. Еще две недели понадобилось на баг‑фикс, всякие удобства и допиливания λC до λD. Как говорил Кнут, «Лучший способ в чём‑то разобраться до конца — это попробовать научить этому компьютер». Именно разработка приложения с нуля даст вам 100%‑е понимание материала, а если вы будете использовать мое приложение — то только 90–95%. Возьмите шрифт Euler и любой HTML‑движок, и этого достаточно для представления любого материала из книги.
Если вы достаточно умный и смелый — можете сразу же прыгнуть на главу 11 в книге по теории типов и программировать математическую логику/решать логические задачи внутри Coq, и возвращаться на предыдущие главы по мере возникновения вопросов. И использовать мои исходники, в которых я на 100% формализовал все содержимое главы и все упражнения в конце главы, для справки и при возникновении трудностей. У меня получилось 700 строк кода, это не очень много. Тут надо еще заметить, что я полностью отключил стандартную библиотеку Coq (опция '‑noinit'), а также не использовал индуктивные типы, которые очень популярны в сообществе Coq‑loving mathematicians.
По поводу первой главы — она довольно емкая и дает основы лямбда‑исчисления. Весьма желательно прорешать ее на бумаге, если вы не имели опыта с теорией лямбда‑исчисления. Coq не совместим с Untyped lambda calculus, так что его не получится использовать для самопроверки. Если вы знаете среду (или язык программирования), которые совместимы с не типизированным лямбда исчислением и позволят формализовать содержимое главы в них и проводить вычисления\проверки, то обязательно напишите об этом в комментариях. Если сможете прорешать первую главу в такой среде — обязательно выложите исходники и пришлите мне ссылку. Я бы сам не прочь вернуться на первую главу и повторить материал.
А что касается аксиоматической теории множеств (ZFC), то у нее есть очень много преимуществ и есть сильная мотивация для ее освоения. ZFC появилась 100 лет назад и на протяжении века все разделы математики были корнями под нее подведены. Любой классический учебник математики можно к ней свести 1–1, даже если неявно на нее не ссылаются. Конечно, есть и другие теории множеств. Например, проект Mizar использует теорию множеств Тарского‑Гротендика (TG), и она немного посильнее ZFC. Но у меня пока не попадалось реальных случаев, когда бы не хватало ZFC.
Если вы хотите короткую серию из вводных лекций по ZFC, я могу вам порекомендовать плейлист от Ричарда Борчердса на YouTube. Он — один из самых крутых математиков в мире, получал Филдсовскую премию в 1998 году — одну из самых престижных наград в математике (ее часто называют «Нобелевская премия для математиков»). Ричард записал бесплатную серию из 8 видеоуроков и разборал все аксиомы ZFC, довольно четко и емко. Я полностью посмотрел и законспектировал его в 2023 году за полторы недели.
Математику часто делят на 2 типа — вычислительную (нахождение производных\решение уравнений и так далее), а также на аксиоматическую (proof‑based/rigorous). Именно второй тип является «настоящей» математикой. Можете почитать про математическую зрелось (Mathematical maturity) и теория типов как раз помогает ее гарантированно достичь. Терренс Тао предложил разделить математическое образование на 3 этапа — Pre‑rigorous/Rigorous/Post‑rigorous. Собственно, формализация математики помогает максимально и идеально прокачать второй этап (Rigorous), и именно на нем обычно застревают большинство студентов.
Я довольно хорошо учился в универе на IT‑факультете (Институт вычислительных систем и программирования (Институт 4) в СПБ ГУАП), и даже получал награду «Студент года ГУАП — 2017». В целом, там была хорошая образовательная программа, но некоторые моменты можно точно улучшить на уровне ГОСТ‑стандартов. Один из таких моментов — это слишком много лекций по теоретическим предметам и отсутствие семинаров по ним с акцентом на покрытие (построение) теории. Пример 1 — у нас был предмет «Абстрактная Алгебра», который был мне интересен. Но семинары по ней не соответствовали тому, что давалось на лекциях — на них мы решали вычислительные задачи вместо доказательства теорем с нуля. Пример 2 — у нас был предмет «Математический Анализ», но на семинарах мы тоже решали вычислительные задачи в большом количестве — нахождение производных и интегралов. Мне кажется, это пережиток прошлого и ГОСТ нужно менять. Лекции, как формат обучения, нужно вообще выпилить. Они имеют очень мало смысла в современном мире. Всегда можно найти записи и просмотр лекции вживую — это, по сути, тоже самое, что и просмотр записи онлайн, только неудобен и будет почти всегда ниже по качеству, чем хорошо подготовленная запись. Вместо лекций, нужно делать много‑много семинаров с небольшими группами студентов по 5–8 человек. Профессор на семинаре может давать тот же материал, что и на лекции, но выводить и доказывать его одновременно со студентами, и делать паузы\давать студентам возможность быть частью этого процесса. Это будет дороже для ВУЗа, но разница вряд ли будет ощутима для руководства.
Еще нужно предупредить вас об одном заблуждении, которое весьма распространено как на Хабре, так и (по всей видимости) среди студентов. Существует пресловутая теорема Геделя о неполноте, которая звучит так: в любой достаточно мощной формальной системе существуют истинные утверждения, которые нельзя доказать в рамках этой системы. И я часто встречал некорректную (неправильную) интерпретацию этой теоремы. Некоторым кажется, что из этой теоремы следует невозможность создания единого фундамента, из которого все выводится. Но ведь такой фундамент есть и уже сто лет существует — и это 9 аксиом ZFC! Можете спросить у ChatGPT, «Какие разделы математики невозможно формализовать в ZFC?» — и он вам накинет весьма редкие случаи, половина из которых (внезапно) из разных глубоких разделов теории множеств. Если вы столкнетесь с этими редкими случаями, вы можете просто накинуть дополнительные аксиомы к ZFC. Например, гипотеза континуума (CH) — вполне себе кандидат на добавление в ZFC, но ее не стали добавлять, т.к. она просто никому особо не нужна. Я не проверял, но полагаю, что можно вывести все ключевые теоремы и утверждения о современных нейронных сетях, и гипотеза континуума при этом не будет использована.
До 2023 года, моей главной целю в изучении теории\фундамента математики было разобраться в фундаменте высокоуровневых математических дисциплин — теории вероятности и математической статистике. Под ними лежит довольно длинный математический стек. Начиная с 2023 года, я переключил главную цель на «разобраться в фундаменте AI». Как выяснилось, эти цели почти полностью совпадают. На основе теории типов вы строим математическую логику, далее на основе логики — строим теорию множеств, затем переходим к построению числовых систем и доказываем существование натуральных чисел на основе аксиомы о бесконечности, далее строим целые и рациональные числа на основе натуральных чисел. После этого можно построить множество вещественных чисел на основе рациональных чисел и перейти к анализу вещественных чисел. Далее, переходим к теории измерений и строим теорию вероятности на ее основе. Далее, независимо от всего этого можно вывести линейную алгебру из теории вероятности. Когда у нас есть теория вероятности и линейная алгебра, можно переходить к математической статистике, а после нее — уже строить конкретные модели нейронных сетей.
Чтобы понять, на каком фундаменте построено современное машинное обучение — можно ссылаться на курсы Mathematics for Machine Learning Specialization (Coursera) и Mathematics of Machine Learning (MIT). Видим, что в списке фигурирует Real Analysis/Linear Algebra/Probability/Statistics/Multivariate Calculus/PCA. У меня сложилось впечатление, что самым важным из этого списка является Real Analysis (вещественный анализ, на русском языке часто его называют просто «математический анализ» или матан), а Calculus III (мультивариативное исчисление) и Probability (теория вероятности) из него выводятся. А статистика, точнее самая вкусная ее часть, выводится из теории вероятности.
Таким образом, центральной задачей в освоении фундамента машинного обучения является формализация математического анализа. Эта задача не нова и решилась еще в 1977 году, когда один студент (аспирант) использовал теорем‑прувер Automath, чтобы формализовать учебник «Основы анализа» (Foundations of Analysis) Эдмунда Ландау и защитил диссертацию на эту тему. Как оказалось, математический анализ очень даже хорошо формализуется. Это очень важный предмет, для понимания которого как раз требуется мыслить через строгую математическую логику, и многие вузы используют его для отсеивания студентов, которые не осилили формальные методы мышления и вместо этого мыслят эмоционально и живут животными инстинктами.
Среди западных авторов, есть 3 хороших учебника по математическому анализу. Самый классический — это Principles of Mathematical Analysis by Walter Rudin, он чаще всего используется в англоязычных технических вузах. Он хорош с точки зрения формальной подачи, глубины проработки и сложных упражнений. Главный недостаток для меня в том, что он аксиоматически задает множество вещественных чисел R (11 аксиом поля и аксиома полноты), вместо того, чтобы выводить все из теории множеств. В этом есть свои плюсы, тк строить всю цепочку числовых систем может отнять много сил и времени. Например, в другом учебнике (Analysis I by Terrence Tao), автор тратит первые 100 страниц книги, чтобы построить числовые системы (N → Z → Q → R) на основе аксиом Пиано. Есть еще книга Understanding Analysis by Stephen Abbott, и у нее очень высокая популярность среди современных студентов (судя по отзывам на амазон). Я прорешал первую главу в 2022 году, но мне она не зашла, т.к. она слишком неформальная и слишком много пробелов\дыр в понимании оставляет. Я бы предпочел потратить в 3–5х больше усилий и пройти книгу Рудина или Терренса, но получить хороший результат без пробелов в понимании.
Собственно, книга Set theory and logic by Robert Stoll от 1963 года тоже строит всю цепочку числовых систем (N → Z → Q → R). Но, как мне кажется, Терренс Тао делает это более подробно и потом плавно перетекает в теоремы анализа, ряды и интегралы. Скорее всего, я пойду именно этим путем, т.к. на основе рядов и интегралов можно потом строить теорию вероятности. Например, в книге A First Look at Rigorous Probability Theory by Jeff Rosenthal, есть раздел «A. Mathematical Background», и автор рекомендует использовать его как измерение «входного порога» (пропускной экзамен) в аксиоматическую теорию вероятности. Если вы чувствуете себя комфортно в тех темах, что там указаны — можно переходить к этой книге. Собственно, там половина — теория множеств, а другая половина — это ряды и свойства вещественных чисел.
Входной порог в аксиоматическую теорию вероятности - что требуется знать
Есть 2 способа формализовать множество вещественных чисел ® — через разрез Дедекина (дается в книге Рудина и Столла) и через последовательность Коши (дается в книге Терренса). Я пока не разобрался в этой теме, но, скорее всего, пойду по второму пути (Cauchy sequences), т.к. это более чистый и современный подход, а также последовательности\ряды более релевантны к фундаменту теории вероятности. Но любой способ подойдет, главное, чтобы на итоговом множестве работали (выводились) аксиомы поля, порядка и полноты.
Что касается линейной алгебры — тут можно ссылаться на учебник Linear Algebra Done Right by Sheldon Axler. Если хотите посмотреть конкретную демку, как главы этой книги формализовать внутри Coq, можете посмотреть плейлист Linear Algebra Done Right in Coq, в котором профессор Квин записал 50 часов видеоуроков. Это может повысить вашу мотивацию и дать конкретный пример. Я планирую повторить тоже самое, но мой фундамент математики будет более чистый (без индуктивных типов), а также полностью выводиться из ZFC.
А если вам нужен хороший курс по Calculus III (мультивариативное исчисление), то я могу порекомендовать курс на Educator (23 часа, довольно емкий и приятный). Я его полностью прошел пару лет назад и научился брать тройные интегралы на бумаге параллельно с автором.
Далее, нужно выяснить, на каком математическом фундаменте построен ChaptGPT. Тут можно ссылаться на курс Neural Networks: Zero to Hero, в котором автор строит GPT-2 с нуля. У меня сложилось впечатление, что математический фундамент генеративных нейронных сетей (внезапно) не отличается от обычных нейронных сетей и уходит корнями в классическое машинное обучение. Но я глубоко не копал эту область, и если я не прав, просьба в комментариях подробно раскрыть эту тему.
Тут надо заметить, что конечный результат работы генеративных нейронных сетей на данный момент является чем‑то типа черного ящика и (насколько я понял) не формализуется. Я думаю, это вопрос времени. Программирование тоже когда‑то считалось скорее искусством, чем наукой. А потом пришел Кнут и подвел четкий математический фундамент под анализ сложности и корректности алгоритмов, переиспользовав при этом существующий математический аппарат алгебры\исчисления\теории множеств и теории графов, а также украв нотацию O большого у Ландау. Я уверен, что с нейронными сетями произойдет тоже самое. Я на 80% уверен, что там будут переиспользованны какие‑то существующие разделы математики, которые уже существуют и полностью совместимы с ZFC. Я на 95% уверен, что даже если появятся новые разделы математики, то их сделают совместимыми с ZFC. Я на 99% процентов уверен, что даже если и появится новый фундамент математики, то его можно будет выразить внутри теории типов и формализовать внутри Coq.
Также, есть интересная книжка Neural Networks from Scratch (https://nnfs.io/), в котором авторы используют только питон и его стандартные библиотеки, чтобы построить простые нейронные сети. Я ее пока не пробовал, но планирую в обязательном порядке попробовать в будущем. Для обучения, именно такие подходы максимально хороши.
Если вам интересна тема прохождения онлайн‑курсов в целом, то я на прошлой работе (когда работал в Сравни Java‑разработчиком) записал большой митап на эту тему, можете посмотреть запись вот тут. А сейчас, я работаю в EDNA Java‑разработчиком.
Анонс моего митапа по онлайн-курсам
Это Ярослав, Java‑разработчик из команды Core/AF. Месяц назад я сделал опрос на тему «Кому интересны онлайн‑курсы?», и увидел большую заинтересованность. Я и Aleksey Dolgushev за месяц проделали большую работу и подготовили интересный и объемный доклад. Уже в эту среду (завтра) с 12.00 до 13.00 будет сама презентация [Sravni Tech Meetup], я проведу ее удаленно для вас (30 минут сам доклад и 30 минут отвечаю на ваши вопросы). В докладе хочу поделиться опытом: за 5 лет я прошел (полностью) более 15 онлайн‑курсов; площадки: Coursera, Educator и TeachIn (МГУ). На встрече обсудим:
— Зачем вообще проходить онлайн‑курсы; какая от этого польза
— Демотиваторы, которые мешают людям проходить курсы
— Про полноценное онлайн‑образование удаленно от топовых ВУЗов мира
— Куда смотреть, где живут правильные курсы
— Как подобрать хороший курс
— Лайфхаки: как получить бесплатный доступ к платному контенту, как не бросить курс в процессе и другие советы
А теперь давайте поглубже поговорим о теории типов. Собственно, Роб в своей книге приводит 11 простых правил выведения типов, которые очень легко запрограммировать и на которых все построено. Он утверждает, что можно взять любой классический учебник по математике и полностью его алгоритмизировать. Любой ход мыслей любого математика, даже самого умного и сложного, можно представить в виде цепочки из N применений этих правил. Если вы взяли любой учебник по теории и не можете каждый его шаг транслировать в маленькие шаги и свести все к логике — то ваша подготовка недостаточно глубокая. Любой (достаточно глубокий) учебник математики = определения + выведение новых результатов на основе предыдущих + небольшое текстовое описание, которое можно выкинуть.
Список из 11 правил выведения типов, на которых все построено
Можете провести параллель с документацией Coq, в которой описано 19 правил выведения обычных типов и еще вот тут 4 правила для выведения индуктивных типов. Coq сильно расширил базовые правила, чтобы было удобнее сопровождать большие проекты по формальной верификации ПО, но при этом остался совместим с золотой классикой исчисления конструкций (Calculus of Constructions).
У читателя может возникнуть вопрос — почему именно 11 правил выведения типов? Может ли их быть меньше? Да, может, есть PTS (Pure Type System), которая стирает границу между термином и типом. Также, есть комбинаторная логика, в которой всего 3 символа (комбинатора) S, K и I. Было доказано, что любые правила выведения типов можно свести с этим 3-м комбинаторам и комбинациям из них. Если вы хотите особо подзапариться, то можете написать движок комбинаторной логики, в которой вы построите 11 правил выведения типов λD на основе этих комбинаторов, а на них уже дальше будете строить все остальное и делать упражнения из книги. Но, на мой взгляд, это уже оверкилл, тк 11 правил λD весьма просты к реализации и пониманию, а также на них основаны теорем‑пруверы Coq и Lean, так что имеет смысл брать именно 11 правил λD за основу.
Тут нужно также заметить, что на каждом этапе можно «срезать углы» и вместо того, чтобы выводить что‑то, можно просто заткнуть дырку аксиомой. Это очень плохо для обучения и глубины понимания, но нужно иметь в виду, что такой подход есть:
Вместо того, чтобы выводить правила и концепции математической логики из теории типов, можно просто накинуть десяток‑другой аксиом. Например, для конъюнкции (A ∧ B) будет 4 аксиомы — одна постулирует существование самой конъюнкции как типа, еще одна на основе A и B выводит (A ∧ B), а другие две на основе (A ∧ B) вытаскивают А и вытаскивают B. Если вы хотите по‑быстрому разработать свой теорем‑прувер на основе логики первого порядка, можете пойти по этому пути. Но лучше все‑таки разобрать правила выведения типов и на их основе все сделать.
Вместо того, чтобы выводить аксиомы Пиано (5 штук) из аксиом ZFC, можно просто их постулировать как аксиомы. Например, Терренс Тао поступает именно так в начале своей книги Analysis I, а иначе его книга могла бы увеличиться в полтора раза.
Вместо того, чтобы выводить всякие концепции типа «пара (a, b)», ее свойство и существование декартова произведения и из теории множеств, можно просто принять их как примитивные и добавить как аксиомы
Вместо того, чтобы выводить всю цепочку числовых систем (N → Z → Q → R), можно сразу же перейти к свойствам R и постулировать существование множества R и аксиомы на нем (поле + порядок + полнота). Многие курсы по математическому анализу именно так и поступают.
Любую слишком большую и толстую теорему в теории вероятности или статистике можно принять на веру и добавить, как аксиому. Собственно, многие курсы и учебники по статистике так и поступают для большинства теорем
Математиков можно поделить на 2 большие группы — алгебраисты и аналисты. Тут можно ссылаться на эксперимент с кукурузкой, в котором показали, что представители этих двух направлений едят кукурузку по‑разному. Мне кажется, что большая часть программистов в индустрии — это алгебраисты, а большая часть статистов/дата‑саентистов — это аналисты. Собственно, школьный предмет «Алгебра и начала анализа» знакомит с основами этих двух направлений. Когда я учился в школе, мне нравилось примерно 60% от того, что мы делали на школьной математике (алгебраическая часть), и я не любил другие 40% (аналитическая часть). Собственно, сейчас я как раз развиваю аналитическое мышление и надеюсь, что мои увлечения фундаментом математики помогут мне овладеть одновременно двумя этими направлениями и есть кукурузку так, как я захочу.
Мне всегда было интересно, как именно происходит переход от алгебраической формы (N = A ∪ ∅) к аналитической форме (p → q → r). На форумах (StackOverflow / Quora) писали, что вся математика может сводиться к небольшому набору аксиом и любое математическое высказывание можно трассировать в виде огромного дерева логических выводов (импликаций), но мне было непонятно, как именно алгебраическая форма вписывается в это дерево. Собственно, в главе 12 «Mathematics in λD: a first attempt» Роб Недерпелт раскрыл этот механизм и ввел йота‑дескрипторы. Получилось очень компактно и аккуратно, всего в 6 строчек вписалось. Он добавил их как 2 «псевдоаксиомы» (примитивные определения), но по сути они не являются аксиомами и не делают теорию типов логически сильнее (и это было доказано). То, что они реально делают — они добавляют «математический сахар» для тех математических объектов, которые (было доказано) существуют и уникальны. Например, вы можете доказать 1 раз, что существует пустое множество и притом только одно, назвать теорему empty_set_unique, и потом ссылаться на это множество через (ι _ (empty_set_unique)): Set. Далее, вы прячете эту йоту под термин ∅, и используете ее так, как ее принято использовать во всех математических текстах. Если вам понадобиться свойство пустого множества, вы можете развернуть термин ∅ обратно в йоту и из нее вытащить свойство.
Собственно, во всех классических математических текстах используют йота‑дескрипторы в неявном виде. Даже ваш школьный учитель математики использовал его много раз на доске, когда писал N и ссылался на уникальное множество натуральных чисел. Под ним прячется йота, а под йотой — доказательство существования этого множества и его уникальности.
Как выглядит йота-дескриптор и его свойство
Можно также посмотреть, как в стандартной библиотеке Coq определяются йота‑дескрипторы. По сути, там тоже самое, но усложненно через использование дополнительных определений и индуктивных типов. Для обучения и понимания\первого знакомства, это усложнение вообще не нужно и сбивает с толку. Это еще одна причина, по которой лучше обучаться по учебнику с акцентом на чистую теорию, а потом уже переходить к конкретной имплементации.
Еще один интересный и простой пример — что такое массив? Что вы видите, как программист, когда думаете о массиве [a, b, c], но без учета порядка элементов? Я всегда видел 3 ячейки в памяти (по 4 байта каждая), которые хранят переменные a, b, c друг за другом. А теперь, я вижу другое — я вижу логическое выражение ∃s. ∀x. ((x ∈ s) ⇔ (x = a ∨ x = b ∨ x = c))). А если учитывать порядок, то это будет функция (множество пар), которая проецирует множество {0, 1, 2} на множество {a, b, c}, т. е. ∃s. ∀p. ((p ∈ s) ⇔ (p = <0, a> ∨ p = <1, b> ∨ p = <2, c> ))). А пару, тоже можно выразить через множество. В общем, в IT все отлично формализуется.
Формализованную математику еще иногда называют механизированной математикой (mechanically checked mathematics). Если вам близок инженерный подход, можете представлять себе математику как огромный завод, на котором в качестве сырья выступает набор из 9 аксиом, а в качестве стандарта сборки — 11 правил выведения типов. Небольшие фабрики производят из этого сырья пруф‑объекты, и потом катят эти пруф‑объекты по ленте к другим фабрикам. Возможно, я переиграл в Satisfactory.
Тут надо еще заметить, что математику (исторически) принято изучать от конкретного к общему. Сначала нужно освоить исчисление (Calculus), понять его применения и выработать интуицию вокруг вычисления конкретных математических объектов и решения конкретных задач, а уже потом переходить к анализу вещественных чисел (Real Analysis). Тут можно ссылаться на провальный эксперимент New Math в США в 1970 году, когда попытались внедрить фундамент математики (теорию множеств и символическую логику) в школьную программу, и заменить ими унылое заучивание таблицы умножения\решение уравнений и так далее. Как выяснилось, это плохая идея — сначала нужно все‑таки сформировать некоторую грязную базу и потратить силы\время на нее (и это наверняка вызовет дискомфорт), а уже потом переходить к чему‑то более абстрактному и чистому.
А теперь поговорим о технических инструментах, которое реализуют внутри себя теорию типов и решают различные практические задачи. Начнем с Coq (он же The Rocq Prover). Он — классика в области формализации математики и формальной верификации ПО. Coq появился в 1984 году и занял эту нишу довольно плотно. Есть и более новый конкурент у Coq — это Lean. Но я не нашел достаточно мотивации, чтобы взять его с самого начала или перейти на него:
Lean построен на той же теории типов, что и Coq, а значит фундаментальных плюсов у него нет.
В документации по Lean я не нашел строгую формулировку правил выведений типов (которая есть у Coq), и это плохой знак.
Lean моложе Coq на 24 года, а значит сообщество и экосистема намного меньше, а также база решенных проблем и применений намного тоньше. Например, у реддита Coq 2500 участников, а у реддита Lean — всего 390.
В Coq вливает много денег большой государственный исследовательский центр во франции (INRIA), а Lean — финансирует небольшой исследовательский отдел Microsoft (но тут я могу ошибаться).
У Coq есть 6-томник «Software Foundations». Ради одного только его я мог бы выбрать Coq
Я выбрал Coq вместо Lean примерно по тем же причинам, по которым я когда‑то выбрал Java вместо С#. Но кроме Coq и Lean, есть и другие теорем‑пруверы. Isabelle/ZF и Metamath тоже все выводят из ZFC, но я их не выбрал в силу их малой популярности, а также слишком кастомного ядра и отсутствия строгой фундаментальной теоретический базы.
У нас есть 3 возможных уровня применения теории типов для формализация математики:
Уровень 1 — мы используем теорию типов только как движок для математической логики, а дальше про нее забываем и работаем полностью внутри математической логики и выводим все математические структуры из аксиоматической теории множеств. Этот подход самый трудозатратный, но он дает самый лучший результат для обучения и глубокого понимания. Поскольку моя цель — это как раз обучение и понимание, я придерживаюсь только этого подхода.
Уровень 2 — мы используем теорию типов не только как движок, но еще и перекидываем некоторые фрагменты теории множеств в нее. Результат получается намного более компактным и удобным для практических задач верификации, но не очень хорош для обучения. Например, вместо того, чтобы выводить множество натуральных чисел из аксиомы бесконечности, мы можем представить натуральные числа как индуктивный тип, или хитро ввести их через йоту. Таким подходом пользуется Роб Недерпелт в его главе по теории множеств, а также он используется в стандартной библиотеке Coq. Мне совсем не нравиться этот подход, так как он ломается на всяких штуках типа «как представить подмножество?» или «как представить множество всех подмножеств (powerset)?» и там приходится костылить.
Уровень 3 — мы полностью переходим в теорию типов и используем ее не только как фундамент для логики, но еще и как фундамент для математических структур. Тут можно отметить работу нашего соотечественника Владимира Воеводского, который развивал гомотопическую теорию типов и даже основал библиотеку Coq для нее. Но это исследовательская область, и у меня пока нет мотивации в нее погружаться. Она настолько не готова, что даже в начале учебника по гомотопической теории типов написано, что теория в процессе изменений и все может поменяться. Возможно, я когда‑нибудь посмотрю курс лекций по теории гомотопии и попробую разобраться, как именно она стыкуется с теорией типов и где это можно применить в моих задачах.
Если вам интересны конкретные применения Coq для решения реальных задач, то можно ссылаться на CompCert — полностью формально верифицированный компилятор языка С. Во время его формализации, исследователи нашли и поправили 100+ критических багов, и как результат — самолеты летают более надежно. Еще есть более свежий проект — CertiKOS, полностью формально верифицированная операционная система, которую невозможно взломать логическими методами. Ее формальная верификация заняла 1 миллион строк кода на Coq. Еще Coq используется в верификации всяких штук в инфобезе типа TLS‑протокола.
Работа по формальной верификации нейронных сетей тоже есть, и я уверен, что это направление будет очень сильно расти в ближайшем будущем. Люди очень боятся восстания машин, так что будут вливать много денег в то, чтобы сделать AI безопасным и надежным. Чтобы дать такую гарантию на 100% — нужны математические методы.
Если вас интересует ситуация в индустрии теорем‑пруверов в целом, то там все очень хорошо. Можно ссылаться на список из 100 самых популярных теорем и списка теорем‑пруверов, в которых они доказаны. Видно, что суммарно покрытие составляет 99 теорем из 100 — каждая из них покрыта хотя бы в одном теорем‑прувере, а на Coq приходится покрытие 79 теорем. Особое внимание можно уделить теореме‑доказательстве иррациональности квадратного корня, которая играет ту же роль, что и «чайник» в 3D графике для проверки движков, и все теорем‑пруверы ее доказывают. Также можно обратить внимание на теорему центрального предела (The Central Limit Theorem), которая покрыта только в теорем‑прувере Isabelle. Сложилось впечатление, что она играет очень важную роль в математической статистике и я пообещал себе, что не вернусь к учебнику по статистике, пока эту теорему не формализую и не пойму до конца, как она работает изнутри.
Еще можно упомянуть проект QED manifesto, цель которого — формализовать и компьюторизовать вообще всю математику. Пока что QED utopia не была достигнута, но максимально к ней приблизился именно проект Mizar Mathematical Library. Я думаю, в будущем к этому проекту вернуться и благодаря AI смогут достичь QED‑утопии. Можете почитать сам манифест, он написан довольно понятным языком и разбирает популярные заблуждения по поводу несовместимости логики, парадоксы и так далее. И аргументирует, что такой проект технически и логически достижим.
Я рекомендую всем, кто умеет программировать, пройти хотя бы первую главу первого тома «Logical Foundations». Она не требует специальной подготовки и займет у вас пару недель. В рамках этой главы, вы построите натуральные числа (N) на основе индуктивных типов, а также их базовые свойства (аксиомы Пиано), и базовые операции (сложение\умножение\возведение в степень\факториал). Также вы познакомитесь с принципом работы Coq и его базовыми тактиками.
Если вы — разработчик в индустрии, то вы, наверняка, привыкли писать императивные программы и лишь изредка использовать функциональное программирование. Хотя на некоторых работах может делаться акцент на функциональщине в силу специфики бизнеса и\или выбранного стека технологий. Например, мы в Edna используем проект Reactor и реактивный подход довольно часто, а на прошлых работах я часто применял Stream API. В случае Java у нас JVM и работа процессора является императивной по своей природе, а функциональное программирование эмулируется внутри императивной модели вычисления (RAM‑модели). А вот в индустрии теорем‑пруверов все наоборот — за основу взята теория типов на основе лямбда исчисления, которая является полностью чистой и функциональной. А императивный подход достигается путем введения языка тактик и автоматизации. Есть 2 способа программировать математические теоремы — напрямую через лямбды, а также через тактики, которые под капотом крутят эти лямбды. Любую теорему Coq можно представить в виде огромной мотни из лямбд. Команда «Show Proof.» печатает вам пруф‑объект (низкоуровневое доказательство теоремы). Coq правда любит прятать их, и нужно через небольшой лайфхак (Defined вместо Qed) определять теоремы, чтобы они не прятались.
Как выглядит доказательство правила Де-Моргана (¬(A ∧ B) ⇒ (¬A ∨ ¬B)) на самом низком уровне
fun (A B : Prop)(H : forall(_ : forall (C : Prop)(_ : forall (_ : A) (_ : B), C), C)(A0 : Prop), A0) =>exc_thrd A(forall (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C), C)(exc_thrd B(forall (_ : A) (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C),C)(fun (H2 : B) (H3 : A) =>H (fun (C : Prop) (h : forall (_ : A) (_ : B), C) =>h H3 H2)(forall (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0,C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0,C), C))(fun (H2 : forall (_ : B) (A0 : Prop), A0) (_ : A)(C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(H0 : forall _ : forall (_ : B) (A0 : Prop), A0, C)=> H0 H2))(fun (H2 : forall (_ : A) (A0 : Prop), A0) (C : Prop)(H0 : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C) =>H0 H2)
Просвечивается exc_thrd — аксиома исключения среднего, через которую и идет доказательство (тк это правило в данной форме — не конструктивно). Других аксиом тут нет.
Собственно, fun — это лямбда и вводится через правило абстракции (abst). forall — это Π‑тип, выводится через (form). Prop — можно заменить на звездочку.
Напечатал путем выполнения команды Eval cbv in deMorganNotAnd. Вот таким нехитрым способом, можно для любой теоремы, доказанной внутри Coq, получить ее лямбда‑форму, развернув все определения.
Особый интерес представляет то, что все учебники из серии Software Foundations интерактивно читаются внутри IDE. Именно таким должен быть учебник математики будущего — на 100% механически формализован и верифицирован, подача учебного материала перемешена с упражнениями, а также есть среда выполнения и язык программирования, которые позволяют экспериментировать\проверять\выходить за рамки. Собственно, тут можно ссылаться на усилия Кевина Баззарда по внедрению теорем‑прувера Lean в имперском колледже Лондона в математические программы (The Xena Project). Я очень поддерживаю такие штуки и думаю, что математическое образование будет именно таким на всех уровнях.
Есть два способа изучать математику — от учителя к ученику (классический подход), а также с компьютером и без учителя (новый подход). Конечно, было бы круто, если бы хорошие учителя были бы доступны по всем предметам, а ученикам было бы приятно и интересно проводить время с ними. Но на практике, есть огромное количество проблем у этого подхода. Они не только финансовые (хороший репетитор\ментор будет очень дорого стоить), но и привязаны к месту проживания (не всегда можно в принципе кого‑то найти в доступности). А также очень трудно найти кого‑то, с кем вам приятно и комфортно проводить время, чтобы человек вам нравился. По итогу, приходится развивать альтернативные направления. Одно из таких направлений — смотреть онлайн‑курсы и видео, в которых у вас создается впечатление, что лектор общается с вами, и вы параллельно с ним прорешиваете задачи, как с репетитором. Другое направление — это всякие интерактивные среды и компиляторы\песочницы, которые строго ограничивают ваши действия и дают информативные сообщения об ошибках, если вы что‑то делаете не так. В этом смысле, теорем‑пруверы типа Coq являются «идеальным учителем» математики, который видит 100% ваших ошибок в логике и просто не даст вам двигаться дальше, если что‑то сделано не так.
У меня есть гипотеза о том, что во время занятия (реальной) математикой у человека в голове формируется что‑то типа теории типов на уровне нейронов. Я пока не могу подтвердить мои догадки и ссылаться на исследования из области нейронауки, но я верю в эту гипотезу и уверен, что в будущем что‑то подобное будет экспериментально доказано.
Еще один лайфхак — если вы девушка и очень хотите войти в айти, то вы можете попробовать пожить с мужчиной, который работает программистом в айти компании (но не со мной) пару лет вместе. Если вы будете каждый день общаться на бытовые темы, вы будете перенимать ход мыслей и впитывать базовые идеи, даже если он вас не будет обучать в явном виде. Это супер‑важно и может сильно вам помочь в развитии потом освоить язык программирования или профессию QA\HR. Но даже если вы ничего не освоите, у вас все равно есть шанс пробиться в айти на большую зарплату. Я периодически встречал коллег, которые ничего не знают\не умеют, но думают как знающий\умеющий человек (мимикрируют под программиста) и хорошо умеют проходить собесы.
А если вы мужчина, то ждите появления виртуальных учителей\менторов на основе GirlfriendGPT, они помогут вам решить главную проблему в образовании — проблему с мотивацией.
А теперь поговорим о теме «войти в IT». Главная причина, почему обычные люди не могут комфортно войти в айти и научиться программировать — это отсутствие математической подготовки и трудности с ее получением. Вот вам секрет, как сделать из обычного человека хорошего программиста: нужно потратить пару лет на школьную математику и подтянуть ее до уровня физ‑мат школ, а уже после этого переходить к языкам программирования. А сразу прыгать на курсы или онлайн‑системы типа JavaRush без уверенной математической базы — это очень плохая идея.
Если вам интересно, откуда я насобирал столько полезной информации по теме фундаментальной математики и связал все воедино, я могу раскрыть мои источники. Я уже 8 лет как активно использую английский Гугл (почти каждый день) и много с ним общаюсь на разные темы. Он дает мне ссылки на английскую википедию, а также на всякие сайты типа MathOverflow, Quora и Reddit. В 2024 ChatGPT созрел как замена Гуглу, поэтому в декабре я купил подписку ChatGPT Plus и перешел на него в качестве дефолтового поисковика в Chrome. Я планирую в 2025 полностью отказаться от Гугла и пользоваться только ChatGPT, переписываясь (или общаясь голосом) с ним на английском языке.
А теперь поговорим о списке практических применений фундаментальной математики. Список довольно большой и он только растет, у меня появляется все больше и больше разных креативных идей каждый месяц. Кажется, у меня все расписано на ближайшие 10 лет и все мое развитие и рост в будущем (как личный, так и профессиональный) будут затрагивать теорию типов\теорию множеств\теорем‑пруверы.
Применение #1: Войти в AI/ML и сделать это по‑царски. По опыту с компьютерными науками я знаю, что чем глубже подготовка по теории — тем лучше. Это не только входной порог, но еще и задел на развитие, более широкий выбор из компаний, возможность миграции внутри компании, гибкость в развитии и резистентность к сокращению. Где‑нибудь в 2026–2027 году я буду готов и сразу возьму какие‑нибудь крутые курсы с Курсеры или MIT OpenCourseWare по AI. Совсем не обязательно полностью формализовать весь фундамент под AI/ML. Я думаю, что глубокое понимание и формализация некоторых ключевых теорем в анализе и теории вероятности будет более чем достаточно.
Применение #2: Алгоритмы и структуры данных, их анализ и формализация. Собственно, я уже итак довольно глубоко проработал эту область и прошел 2/4 курса из специализации на Курсере по дизайну и анализу алгоритмов от Стендфордского университета в 2022 году. Моя главная цель — это не только комфортное прохождение алгоритмических собесов и сильная позиция на рынке, но еще и возможность брать более крутые и интересные задачи. Я пока не знаю, как именно буду продвигаться дальше, но я точно знаю, что хочу формализовать машину Тьюринга внутри ZFC и научиться ее там крутить, а также разобраться, как именно RAM‑модель (математический ассемблер) компилируется в машину Тьюринга. Если это сделать, то можно добиться 100-го понимания самой концепции алгоритма и, как результат, получить большой бонус к решению алгоритмических задач. Будет идеально, если я смогу на LeetCode решать алгоритмические задачи одновременно на двух языках — математическая модель и доказательство корректности\сложности на Coq, и быстрая имплементация алгоритма на Java.
Входной порог в алгоритмы и структуры данных - что требуется знать
Взял из CLRS
Тут еще надо заметить, что среди программистов в России очень много слабых IT‑специалистов с очень слабой математической подготовкой, которые решают весьма рутинные и неинтересные задачи в проектах с кодовой базой плохого качества, а также не хотят изучать что‑то новое и вкладываться в развитие. Такой путь развития и раньше был не перспективен, а теперь (с учетом изменений в мире AI) кажется совсем провальным и я вам крайне не рекомендую прислушиваться к мнению таких знакомых, если они у вас есть.
Применение #3: Формализация программного обеспечения. Как я уже писал, Coq активно используется в индустрии для того, чтобы доказать корректность работы программ и вообще любых IT‑систем. Я изначально думал, что это слишком узкое направление и в целом не очень полезное для карьеры Java‑разработчика. Сейчас я так не считаю. В моей работе регулярно встречаются ситуации, которые критически важны для бизнеса и которые прямо таки напрашиваются, чтобы их формализовали. Формализация позволит не только дать более четкий\аргументированный ответ бизнесу (актуально для техлида), но и предотвратить инцеденты на проде (и отдыхать вместо того, чтобы их исправлять). Например, микросервисное взаимодействие и некоторые архитектурные паттерны прямо так и напрашиваются, чтобы их формализовали. Компании тратят куча денег и ошибки — стоят очень дорого. Лучше убедить бизнес, чтобы эти деньги положили Java‑разработчику в карман.
Собственно, я полтора года назад прорешал первые 6 глав на 100% в учебнике Logical Foundations, но застрял на главе «Inductively Defined Propositions», тк она (по всей видимости) — повышенного уровня сложности. На тот момент у меня не было такой глубокой теоретической подготовки, как сейчас. Сейчас я могу вернуться и закончить первый том. В ближайшие пару лет сделаю, если не будет более интересных приоритетов.
Применение #4: Формализация баз данных. Базы данных используют вообще все специалисты в IT (даже менеджеры), и возникает очевидный вопрос — а как формализовать реляционные БД? В 2021 году я наткнулся на очень крутую книгу Applied Mathematics for Database Professionals by Lex deHaan, в которой авторы очень чисто формализуют современную БД и язык SQL в терминах математической логики и теории множеств. Эта книга была для меня большим открытием и я довольно быстро и комфортно прорешал первые 8 глав и упражнения к ним на бумаге. Она не только покрывает простые CRUD‑операции, но и более сложные темы, такие как структура БД, ее ограничения и транзакции.
Собственно, это очень полезно для более глубокого понимания логической сути БД (что в БД важно, а что второстепенно), помогает не утонуть в деталях имплементации конкретной БД, а сконцентрироваться на ключевых моментах и более грамотно проектировать БД.
Пример Select и его формальная форма на языке теории множеств
select distinct e.JOB from EMP e where e.MSAL > 4800 or e.SGRADE >= 6
Входной порог в теорию БД - что требуется знать
Применение #5: Развитие в менеджмент. У меня сложилось впечатление, что хорошие менеджеры (особенно топ‑менеджеры) — это весьма образованные люди и они максимально используют математику в работе. Речь идет не только о простом статистическом анализе данных, но еще и о построении и проверке гипотез, использовании инструментов Data Science, а также применении всяких интересных штук типа Теории Игр/Теории оптимизации/Линейного программирования для принятия крупных стратегических решений. Собственно, можно попробовать развиваться по этому пути и заработать очень много денег, которые многократно окупят затраты на фундаментальную математику. Можно также попробовать соединить теорию менеджмента, сертификацию PMP и генеративные нейронные сети, чтобы сделать что‑нибудь интересное и креативное.
Тут я хочу заметить, что среди знакомых я встречал много примеров плохих менеджеров — которые уходят в менеджмент из‑за профессиональной деградации и лени, получают зарплату сильно меньше хорошего программиста, а также используют весьма примитивные инструменты и личный (иногда эмоциональный) опыт в принятии решений. Такой путь развития я в принципе не рассматриваю, и под словом «менеджер» я подразумеваю именно математического менеджера, которого я описал в абзаце выше.
Применение #6: Разработать свой 3D движок и свою 3D игру. Я начал программировать в 13 лет с разработки своих игр и 2D движков для них в 2007 году. С тех пор я мечтаю попробовать разработать свою 3D игру — как хобби и для удовольствия. Мне все равно придется глубоко осваивать линейную алгебру для ML, а в качестве бонуса и мотиватора можно сделать свой 3D движок с полного нуля и с полным пониманием фундамента.
Применение #7: Глубоко понять доказательную медицину. У меня сложилось впечатление, что лучшая часть медицины — это та, что базируется на математической статистике. И медицина будущего будет именно такой, ее нужно полностью свести к статистике и теории вероятности. Мне очень интересно это направление и ради только его одного я мог бы потратить пару лет на обучение. Математика может не только помочь интуитивно понять сложные исследования и статьи в медицине, но еще и попробовать всякие интересные проекты, типа Hummod (cамая полная математическая модель физиологии человека из когда‑либо созданных).
Применение #8: Глубоко понять, как устроен реальный мир на низком уровне. У меня еще со школы сохранилась мечта — написать программу, которая из законов квантовой физики выводит таблицу Менделеева и предсказывает химические реакции, а также закладывает фундамент химии. Но на тот момент, у меня не хватало ни алгоритмов, ни глубокого понимания квантовой физики и ее математической базы. Собственно, в ближайшем будущем я могу попробовать освоить и формализовать дифференциальные уравнения и дальше сделать что‑то типа симулятора квантового мира. Но когда у меня до этого руки дойдут — не знаю. Сейчас мне 31 год, и столько всего нужно изучить и попробовать, много других приоритетов есть. Возможно, когда мне будет 50+, я вернусь к этому вопросу.
Применение #9: Написать убер‑диссертацию на тему математического фундамента ChatGPT. Собственно, я уже учился в аспирантуре ИТМО (2017 — 2020) на кафедре информатики и прикладной математики (ИПМ), но на тот момент у меня не было реального исследовательского проекта, так что я сдал академический минимум и ушел. По мере накопления математического фундамента, я понимаю, что он идеально подходит для написания диссертации. Будет круто, если у меня реально получится пройти весь путь от теории типов до теории генеративных нейронных сетей и получить PhD в этой сфере. Но когда у меня на это появится свободное время — я не знаю. Я думаю, что скорее восстание машин начнется, чем я успею защитить диссертацию...
Моя главная цель при написании этой статьи — получить как можно больше отзывов и обратной связи и скорректировать\дополнить\расширить мои планы на будущее. Буду рад услышать ваши замечания, рекомендации, советы и критику. Чем больше напишите, чем лучше. Можете писать в комментариях, на почту (kciray8@gmail.com) или в Телеграм личным сообщением.
Комментарии (127)
andreykl
01.01.2025 10:25> Натуральная Дедукция.
Естественный вывод.
Martin-Löf type theory (MLTT) и Calculus of Construction (CoC)
Он всё таки различаются. К примеру, MLTT предикативна (вроде бы?). А в CoC (в смысле Coq) есть импредикативный Prop. На сколько я понимаю раньше и Set был импредикативен.
kciray Автор
01.01.2025 10:25По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
Про импредикативность Coq вы все правильно написали. Да, MLTT предикативна, а CoC и Coq - как правило, нет (но есть чит-опция). Какие это имеет последствия - я пока не ощутил.
andreykl
01.01.2025 10:25> По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
В целом вы правы. Но по неправильной причине :). Не то что бы дело в противоречиях. Дело в принятых терминах. Я человек к логике отношение имеющий постольку поскольку и думал что верный термин "естественный вывод". И он верный. Но "натуральная дедукция" тоже легко гуглится и по всей видимости это вполне устоявшийся термин. Ещё встретил "Натуральный вывод".
Так что я поторопился с поправкой.
Coq - как правило, нет (но есть чит-опция)
Coq имеет предикативную систему для Type и импредикативную для Prop. (Ещё можно сделать Set импредикативным с помощью опции).
Насчёт чит-опции я не в курсе, поясните, пожалуйста.
kciray Автор
01.01.2025 10:25Под чит-опцией я как раз и имел в виду ту опцию, что делает Set импредикативным
andreykl
01.01.2025 10:25В целом очень интересный обзор (и личная история успеха). Просмотрел пока, думаю вернусь к чтению, любопытно побольше узнать про опыт, похожий на собственный (лет 6 назад).
SairusKR
01.01.2025 10:25Приятно видеть, что есть люди, видящие настоящую красоту математики.
Сразу скажу, что у меня только общие представления. Насчёт теории категорий, то насколько я знаю это удел алгебры. Т.е. в категориях акцент ставится именно на изучение операций между объектами, а не самими объектами (складывать можно и матрицы и числа - значит фундаментальнее рассматривать сложение, а не разные объекты).
По поводу ZFC, то мне как-то не верится, что она может вывести аксиомы геометрии Гильберта, топологии и теории чисел. Если из нее можно выразить алгебру, матанализ, логику, теорвер, то это и вправду фундаментальная вещь (правда, если она выражает арифметику/ аксиомы Пеано (она тьюринг-полна), то проблема остановки и теорема о неполноте (почему Вы ее как-то обделили) говорят, что не выйдет построить машину выводящую все теоремы. Это можно будет сделать только для довольно маломощных систем аксиом (например евклидова геометрия)).
Кстати кто-то даже пытался свести все аксиомы математики в одну универсальную (тут).
kciray Автор
01.01.2025 10:25По поводу ZFC, то мне как-то не верится, что она может вывести аксиомы геометрии Гильберта, топологии и теории чисел
Вот я тоже не верил, что аксиомы Пиано на натуральных числах можно вывести, а потом взял и вывел (по учебнику). Мне кажется, что теория чисел должна очень даже хорошо и чисто формализоваться, т.к. нам осталось вывести множество Z и это хорошо решаемая задача, когда представляем каждое число в виде класса из пар двух натуральных чисел (a, b).
По поводу топологии и геометрии Гильберта, я поговорил с ChatGPT, он утверждает, что классическая часть этих областей без проблем выводиться из ZFC, а глубокие штуки на стыке с теорией множеств, связанные с гипотезой континуума или большими кардинальностями - нет. Собственно, что и следовало ожидать.
https://chatgpt.com/share/6775381f-9424-800e-b161-938164dde4d9
Zenitchik
01.01.2025 10:25я поговорил с ChatGPT
А с помощью чего Вы валидировали его ответ?
kciray Автор
01.01.2025 10:25А никак не валидировал, принял на веру =). Если кто-то глубоко шарит в топологии или геометрии Гильберта, просьба прокомментировать.
Но по теории чисел - я зуб даю, что прокатит ее очень чисто формализовать
Zenitchik
01.01.2025 10:25Вы когда-нибудь пробовали поговорить с ним, например, о генеалогии монархов Европы? Или о художественной литературе?
ГПТ может запросто написать неправду. В смысле 100%-ый вымысел. Поэтому его обязательно нужно валидировать.
Dhwtj
01.01.2025 10:25Нашел перевод одной из упомянутых книг
kciray Автор
01.01.2025 10:25Посмотрел. Да, перевод есть, но он 7-ми летней давности (книга много обновлялась) и не все главы переведены, например IndPrinciples.v только заголовки переведены. Впрочем, это не проблема - можно скормить эти исходники какому-нибудь переводчику и он должен легко справиться с переводом, так как исходники книги - доступны
ednersky
01.01.2025 10:25теория типов удобна для компьютера
много встречаю это утверждение, но доказательств, увы, не видел.
да типы нонче в моде, однако чтобы они были удобны - этого я не вижу.
где на бестиповом языке писали 1-2 строки, на типовом теперь пишут 1-2 экрана да и ещё иммутабельность пропагандируют, с которой 1-2 экрана превращается в 5-10.
с типами компиляторы писать проще, и линтеры - это да.
однако если переложить всю (вообще всю) работу на программиста, то и компиляторы можно не писать. круто же?
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
gonzazoid
01.01.2025 10:25Строгая типизация (с нормальной системой типов) заменяет юнит тесты и эта замена равносильна 100% покрытию. Если вы тесты не писали то разница будет не так очевидна.
ednersky
01.01.2025 10:25Строгая типизация (с нормальной системой типов) заменяет юнит тесты
нет.
я много спорил на эту тему на хабре, но мне всегда приводили в пример цикл, генерирующий ряд Фибоначчи.
Я спрашивал "где применяется ряд Фибоначчи". Увы, в ответ слышал лишь тишину.
Я просил, чтобы мне показали http-сервер без тестов, но мне не показали. Увы. Примеров не было.
и эта замена равносильна 100% покрытию.
у нас мир реальных приложений:
клиент приходит с запросом от браузера
запрос разлетается по X микросервисам
микросервисы представляют мутабельный API
и так далее
в типы можно уложить только что-то сферическое и в вакууме.
gonzazoid
01.01.2025 10:25Вы же видите что я про юнит тесты говорю - зачем вы мне интеграционные в пример приводите?
ednersky
01.01.2025 10:25потому что во первых есть понятие юнита. Что такое юнит? это файл или на (ОЧЕНЬ) худой конец - функция.
Википедия: Модульное тестирование, иногда блочное тестирование или юнит-тестирование (англ. unit testing) — процесс в программировании, позволяющий проверить на корректность отдельные модули исходного кода программы, наборы из одного или более программных модулей вместе с соответствующими управляющими данными, процедурами использования и обработки.
А во-вторых, далеко не все функции сводятся к чистым (моё эмпирическое мнение - не более 1% в реальном мире)
Соответственно юнит-тест - тест, тестирующий все функции юнита, ну или хотя бы одну, но любую.
Тест для функции, сохраняющей данные в файл - такой же юниттест, как и тест для функции, генерирующей ряд Фибоначчи.
И поскольку чистых функций, как сказано выше, не более 1%, то от юниттестов отказаться невозможно. И польза у типов "быть альтернативой юниттестам" становится весьма сомнительной.
IUIUIUIUIUIUIUI
01.01.2025 10:25А во-вторых, далеко не все функции сводятся к чистым (моё эмпирическое мнение - не более 1% в реальном мире)
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Ну либо решаемые задачи — «принять жсон отсюда и переложить как есть туда». Не знаю, что в таком случае тестировать или обкладывать типами (хотя параметризм мог бы помочь).
Тест для функции, сохраняющей данные в файл
Эта функия называется
Data.ByteString.Lazy.writeFile. Что вы там тестировать собрались? Она уже протестирована авторами библиотекиbytestring.Ну и по предыдущему комментарию:
Я просил, чтобы мне показали http-сервер без тестов, но мне не показали.
Когда-то давно писал тестовым заданием на прикладного хаскелиста маленькую http api-шку, которая получает картинку, распознает там объекты и складывает в БД (а потом возвращает обратно, если что).
Сервер — поверх servant. Там (в самом сервере) просто нечего было тестировать, все типами описано и компилятором проверяется.
А тесты были только уровня интеграционных и только для «бизнес-логики», которая вполне себе реализуется чистыми функциями, и которую так писать даже удобнее, опять же. В более выразительном языке и это можно было бы покрыть типами.
kciray Автор
01.01.2025 10:25Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Бешено плюсую
alhimik45
01.01.2025 10:25Начал сильно обращать на это внимание только после работы с системами типа Temporal/Azure Durable Function где фреймворк форсит тебя разделять decision-making и грязные дествия.
Мысль кажется очевидной когда осознаешь её, но как же в обычных языках типа C#/Java блин проще не задумываясь, в потоке, написать всё в одном классе, максимум в приватные функции выделив обращение во внешний мир. И получить непокрываемую юнит-тестами логику :(
Выносить сайд-эффекты в отдельный класс, прятать за интерфесом, чтобы в тестах замокать. Ещё придумывать какие типы будут в интерфейсе, тупо брать модели из используемого клиента внешнего сервиса из реальной имплементации или создавать отдельные модели и делать конвертацию между ними. Оно в целом недолго делается, но ментально это настолько больше шагов что порой проще сказать "да интеграционными тестаи проверится за компанию". Может есть какой-то более простой рецепт как всё это разделять, который я не вижу?
qw1
01.01.2025 10:25Бизнес-логика часто максимально тривиальная, типа
votes[voteId]++;Тесты на это делать как-то смешно.
А всё остальное - обвесы с эффектами: чтение из хранилища, запись в хранилище, синхронизация между потоками, сериализация/десериализация.
Если в бизнес-логику начинает вклиниваться какой-то нетривиальный алгоритм, типа вычисления необычной контрольной суммы, или поиска кратчайшего пути, его надо выносить в библиотеку и её покрывать тестами.
kciray Автор
01.01.2025 10:25блин проще не задумываясь, в потоке, написать всё в одном классе
Так делать точно не нужно. Это будет страшный спагетти-код. Помимо простого деления на бизнес логику и работу с вводом\выводом, есть еще и другие слои, например работу с БД принято выносить в DAO-классы. Интеграции с внешними системами - тоже в отдельные классы и отдельные пакеты. Иногда даже в отдельные библиотеки. А еще, принято использовать паттерны проектирования, и они, как правило, тоже выносятся в отдельные классы
alhimik45
01.01.2025 10:25Не, я имел в виду "всё" одного уровня абстракции. Ну то есть условно код, который по бизнес-логике должен составить запросы в сервис1 и сервис2 и по данным от них либо вызвать одно действие в сервисе3 либо ещё забрать данные из сервиса4 и уже с ними вызвать сервис3.
Клиенты к сервисам естественно отдельные классы/модули. Иногда это можно разделить так, что вначале сделать все внешние запросы и потом вызвать чистую логику принятия решения что отправлять в сервис3. Но если вызов в сервис4 дорогой, то его надо делать только если действительно нужно. А определение нужности уже часть бизнес-логики. И тут либо мокать клиенты к сервисам, получая связанность теста с конкретными деталями взаимодейтсвия с сервисами и меняя его если бизнес логика какой-нибудь FindById сменит на вызов FindByUsername. Либо абстрагировать всех клиентов за специальным интерфейсом созданным специально для этой части бизнес-логики. Тогда бизнес логика вызывает только этот специальный интерфейс, который можно замокать в тестах и изменения лишь особенностей взаимодействия с внешним миром (поменять имплементацию interface.FindUser c client1.FindById на client1.FindByUsername) не приведет к изменениям тестов.
Но пилить отдельный интерфейс для каждого workflow такого вида - выглядит громоздко
ednersky
01.01.2025 10:25фанатизм в моде нонче
бешено плюсуем, бешено преследуем несогласных
скрепность, духовность, сектантство, бастилии и репрессии
война никогда не меняется...
ednersky
01.01.2025 10:25это не я живу в нечистом мире, это Вы пытаетесь от него абстрагироваться
что-то полезное (чтоб прямо были люди, которые пользуются) написали?
вот тем, к чему я руку приложил, вы точно скорее всего пользовались: яндекс. такси, яндекс.лавка.
но там вообще и запаха типов и иммутабельности нет, уж извините.
а что сделали Вы?
очередную инкарнацию Фибоначчи?
IUIUIUIUIUIUIUI
01.01.2025 10:25Аргументы по существу кончились (вернее, их и не было изначально), и пошёл спердоб/адхом? Ну как хотите.
это не я живу в нечистом мире, это Вы пытаетесь от него абстрагироваться
Да, потому что, ещё раз, тогда проще и разрабатывать, и тестировать, и рассуждать о коде. Это (более частными терминами и с большими костылями) пишут в каждой первой книжке по архитектуре ПО — dependency injection, SRP, какая-нибудь там гексагональная архитектура, и прочая ерунда.
Короче, не вижу в этом ничего плохого. А вот так патологически бороться за говнокодинг, как вы это делаете — это я не очень понимаю. Зачем так делать?
вот тем, к чему я руку приложил, вы точно скорее всего пользовались: яндекс. такси, яндекс.лавка.
А, понятно, зачем. Просто вы — из того сорта яндексистов, которые наслаждаются своей элитарностью, которая им даруется местом, где они просиживают штаны и говнокодят (ведь они же прошли все литкод-интервью в Яшечку!). Притом, что говнокодинг в Яндексе — это тоже притча во языцех (фокус на литкодинге к другим результатам и не приводит). Я бы не хотел идти работать в Яндекс.
И нет, не пользовался ни одним из них.
но там вообще и запаха типов и иммутабельности нет, уж извините.
Здесь мы обсуждаем чистоту. И расчёт путей и цен — не чистая задача? Поиск ближайших таксистов и соотнесение их с заказчиками — не чистая задача?
а что сделали Вы?
Ничего, конечно же. Я ж только языком трепать могу, сорьки, куда мне до Маэстро Литкода.
ednersky
01.01.2025 10:25Аргументы по существу кончились (вернее, их и не было изначально)
кончились они, когда меня стали поучать: «так делать надо, а так — нет»
я просил аргументов, а что получил? высокомерное «п-ф-наставление»?
так наставить и я могу, благо мой опыт ХОТЯ БЫ релевантен :)
А вот так патологически бороться за говнокодинг, как вы это делаете — это я не очень понимаю.
знаете, как, например, появилась Яндекс-лавка?
бизнес сформулировал идею
обкатал её на одном (прописью: одном) складе, без софта (1с и excel не в счёт)
встал вопрос «как это масштабировать»
пришли умники «делать всё правильно» и выдали срок: 20 человек будут работать и к лету 2022 года будет MVP
пришёл я и выдал срок: март 2021, делаю «неправильно» и мне надо всего три (прописью: три) человека
и в марте 2021 — самый разгар ковидных ограничений, у нас работало 100+ складов в Москве.
и ежедневно открывался новый
говнокодинг? так я сразу об этом заявил: будет монолит (оно и теперь так остается)
а за 2021 год Я.Лавка заработала 24 млрд рублей.
представлял бы НЕговнокод ценность иную, нежели ряды Фибоначчи — переписали бы, благо на говнокоде столько бабла подняли, что хватило бы...
прибыли, понимаете, похрен: говнокод там или нет
впрочем, прибыль она говнокод предпочитает, ибо на нём решение на рынок выходит на год-три раньше.
такие дела
ps: а сейчас в лавке НЕговнокодит уже около 100 человек. Но клиент не видит результатов их труда, увы
IUIUIUIUIUIUIUI
01.01.2025 10:25я просил аргументов, а что получил?
Нет, вы не просили аргументов. Вы сказали, что ваше эмпирическое мнение — что всего лишь 1% функций чистые. На это я ответил, что либо вы неправильно декомпозируете задачу, либо просто у вас такие задачи, где бизнес-логики толком нет, а есть только перекладывание жсонов.
В ответ на это можно было бы рассказать, например, подробности про решаемые задачи, а вы зачем-то стали пускать пыль в глаза про Яндекс.Лавку.Такси.Алису.
высокомерное
Лол, с такой чувствительностью к критике картина становится всё более цельной.
знаете, как, например, появилась Яндекс-лавка?
Не знаю и не очень интересно, потому что дальше снова какое-то непроверяемое пускание пыли в глаза, которое вообще не имеет никакого отношения к долгосрочной поддерживаемости кода (как вам расскажет любой эффективный менеджер, срезающий косты и рапортующий об успехах, а после него — хоть потоп).
а сейчас в лавке НЕговнокодит уже около 100 человек. Но клиент не видит результатов их труда, увы
Подчищают за вами, видимо.
У меня тоже такой пример перед глазами есть. Был на одной моей работе чувак, и начал он разрабатывать одну, скажем, фичу. Пре-MVP выкатился очень быстро, потому что чувак максимально срезал углы. Про это написали в анонсе новой версии, бизнес пипл что-то там оценили, что это привлекло 100500 новых клиентов и денег и вызвало энтузиазм, и все радостно получили бонусы.
Проблема в том, что чувак срезал углы. Поддерживать и развивать эту кодовую базу за пределами пре-MVP было очень больно: добавляешь что-то в одном месте, так в другом разваливается. С этого проекта за моё время там ушло трое других людей потому, что над ним невозможно работать, не удалось найти никого другого, кто хотел бы им заниматься, бизнес пипл пришлось всё время придумывать, почему обещанные фичи не реализуются, исходный чувак с бонусом и красивой строчкой резюме упорхал в следующую компанию, а исходные менеджеры, выписавшие ему и себе бонусы, тоже куда-то там упорхали.
Но да, в глазах общественности чувак молодец и гений, а все остальные — туповатые лентяи, раз ничего не могут после него сделать.
прибыли, понимаете, похрен: говнокод там или нет
Ещё выгоднее веществами барыжить или там, не знаю, pump & dump на шиткоинах. Может, ну его нафиг это программирование?
ednersky
01.01.2025 10:25В ответ на это можно было бы рассказать, например, подробности про решаемые задачи, а вы зачем-то стали пускать пыль в глаза про Яндекс.Лавку.Такси.Алису.
к Алисе я не имею никакого отношения и не знаю про неё ровным счётом ничего. Но если мне приведут в пример Алису, я смогу представить какой там уровень задач, с чем сталкиваются программисты и так далее.
с Лавкой и Такси тоже всё примерно понятно: у вас есть приложение, вы отправляете заказ, где вам находят свободного исполнителя, который этот заказ исполняет.
любой программист, который соберётся запрогать - поймёт что и как.
но если интересны подробности, то в такси был большой картографический блок (с нуля написанный) плюс система сбора/хранения координат/треков водителей, при том, что по ней нужно быстро искать понятие "ближайший".
Некоторым боком там была задача комивояжёра.
которую мы решали методом "х-к х-к и в продакшен"
Знаете какой самый козырный и самый масштабируемый способ её решать? Если конечно плевать на перфекционизм? И, главное, не лезть во всякие градиентные спуски и прочую псевдоматематическую ненужность.
PS: вообще, математика программистам ни разу не нужна. для развития мозга её изучать, разумеется, полезно, но в работе в среднем она нафиг не сдалась.
Подчищают за вами, видимо.
точно-точно! переписывают на микросервисы. код, что был написан в период с октября 2020 по март 2021 тремя (прописью: тремя) человеками. с тех пор вот и переписывают.
а там всё просто: шардированный постгрис на котором построена учётная система и решение задачи "продажи последнего билета" ну и несколько рабочих мест: кладовщика/экспедитора/итп/итд.
"чистых функций" около нуля. Покрытие тестами около 80%. Нет, их (чистые функции), конечно, можно выделить в отдельные сущности, но тогда количество кода в системе удвоится. Оно надо? Оно никому не надо. Потому и не парятся - так живут: перепишут на микросервис кусок - потом назад откатываются. Зарплата платится, бонусы за ревью выдаются - что ещё надо программистам?
IUIUIUIUIUIUIUI
01.01.2025 10:25но если интересны подробности, то в такси был большой картографический блок (с нуля написанный) плюс система сбора/хранения координат/треков водителей, при том, что по ней нужно быстро искать понятие "ближайший".
Звучит как чистые функции.
Некоторым боком там была задача комивояжёра.
И это тоже.
которую мы решали методом "х-к х-к и в продакшен"
Не ожидал другого.
Знаете какой самый козырный и самый масштабируемый способ её решать? Если конечно плевать на перфекционизм? И, главное, не лезть во всякие градиентные спуски и прочую псевдоматематическую ненужность.
Да конечно не нужно. Это всё вообще никогда не нужно.
Я недавно форму заполнял на 6 экранов и примерно сотню полей суммарно, и к концу её валидация занимала минуты две при каждом изменении формы. Почему? Потому, что литкод-маэстро нечистых функций, её писавшие, тоже сделяли х-к х-к и в продакшен, и в итоге у них там алгоритм Шлемиеля, ведущий к тому, что первое поле проверяется при проверке первого, второго и последующих, второе — при проверке второго и последующих, и так далее, и в итоге O(n²) на ровном месте. И на каждое поле они отправляли запрос на сервер и обратно.
Зачем? Почему? Потому, что на их игрушечных данных всё работало, можно релизить MVP!
точно-точно! переписывают на микросервисы
Какое отношение микросервисы имеют к обсуждаемому вопросу?
Покрытие тестами около 80%.
До сих пор не понимаю, зачем тесты писать. Только замедляют работу :shrug:
ednersky
01.01.2025 10:25Я недавно форму заполнял на 6 экранов и примерно сотню полей суммарно, и к концу её валидация занимала минуты две при каждом изменении формы. Почему?
это как раз от внедрения всех этих типов во фронтенд.
и от внедрения именно чистых функций.
почему так? а потому что чтобы упростить код, писатели "на чистых функциях" стоят перед развилкой: либо написать независимый чекер к каждому элементу, либо тупо пересчитывать весь список целиком.
в итоге:
вы вводите input текст, он декларативно отображается в значении некоторой переменной
но от этой переменной любители иммутабельности и числых функций отказались и вместо сотен переменных у них она всего одна (типа минимизировали количество грязи)
затем на её изменение сработал триггер из чистой функции и пересчитал DOM-дерево вашего браузера. Целиком.
Вот и получается, что из-за войны за чистоту мы имеем ситуацию, где в ответ на ввод одного символа браузер перелопачивает мегабайты текста.
IUIUIUIUIUIUIUI
01.01.2025 10:25почему так? а потому что чтобы упростить код, писатели "на чистых функциях" стоят перед развилкой: либо написать независимый чекер к каждому элементу, либо тупо пересчитывать весь список целиком.
С чего это? Не упрощает это код и нет такой необхоидмости.
затем на её изменение сработал триггер из чистой функции и пересчитал DOM-дерево вашего браузера. Целиком.
Нет, это не на изменение. Это на нажатие специальной кнопочки «check for errors».
ednersky
01.01.2025 10:25С чего это? Не упрощает это код и нет такой необхоидмости.
с факта тормозов
не было бы необходимости - почему бы 90% сайтов так тупили?
IUIUIUIUIUIUIUI
01.01.2025 10:25А, я понял! У вас типизация и разделение обязанностей просто ответственны за все смертные грехи. На улице гололёд — тоже хаскелисты виноваты полюбас.
ednersky
01.01.2025 10:25типизация - да
про разделение обязанностей я ничего не говорил
типизация - результат поветрия, моды.
какой-то умник сказа[ну]л: goto плохо и понеслось: goto плохо, goto плохо
потом другой умник сказа[ну]л: исключения плохо
потом третий: типизация хорошо
под всеми этими высказываниями не лежит никакой пользы, они все вредительские
kciray Автор
01.01.2025 10:25Спасибо за интересное обсуждение. Про мир реальных приложений (запрос к веб-приложению и микросервисы) - это как раз то, чем я профессионально занимаюсь на основной работе как Java-разработчик уже много-много лет. Хочу вам сказать, что строгая типизация для высоконагруженных бэкенд-приложений просто жизненного необходима, она очень много ошибок предотвращает. Например, мы на работе очень часто задаем, что запрос пользователя должен быть строго по спецификации (ООП иерархия объектов) и некоторые поля обязательно должны присутствовать, другие должны иметь минимальную длину и так далее. Например, аннотации javax.validation используются.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Да из личного опыта программирования этой теории типов - 11 правил выведения типов довольно легко запрограммировать. А вот если вы теорию множеств захотите запрограммировать - все не так просто, там придется теорию типов вводить\придумывать к ней.
IUIUIUIUIUIUIUI
01.01.2025 10:25где на бестиповом языке писали 1-2 строки, на типовом теперь пишут 1-2 экрана да и ещё иммутабельность пропагандируют, с которой 1-2 экрана превращается в 5-10.
А почему не 50-100?
Аннотации типов в большинстве мейнстримных языков с продвинутой системой типов нужны мало где, поэтому оверхед по писанине от типизации сильно меньше (а при чтении он из оверхеда превращается во благо, кстати), и он существенно меньше, чем выигрыш на становящихся ненужными тестах.
с типами компиляторы писать проще
И снова нет. Тайпчекер — весьма нетривиальная часть компилятора, и куда проще просто забить и напихать рантайм-проверки.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения, тем быстрее при прочих равных будет ваша программа.
kciray Автор
01.01.2025 10:25Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения,
Плюсую, языки программирования именно этим путем развиваются. C++ -> Java -> Kotlin все больше и больше проверяют на этапе компиляции. Дошло до того, что Kotlin банально заставляет вас прорабатывать все null-типы через if, чтобы потом на проде не словить NPE
ednersky
01.01.2025 10:25минусую
вижу стектрейсы и паники в гошных приложениях, равно как и в приложениях на расте
вижу тип any, который понемногу но завоёвывает гошку (несомненно хорошее движение — в сторону KISS принципа)
вижу внедрение вопросиков в раст, потому что возня с ошибками всех задолбала: мир понемногу возвращается к варианту — плевать на ошибки в коде, отлавливая их где-нибудь "наверху": грохнулось — перезапустили, а потом на статистику ошибок поглядели и что-то поправили, или даже оставили так
IUIUIUIUIUIUIUI
01.01.2025 10:25плевать на ошибки в коде, отлавливая их где-нибудь "наверху": грохнулось — перезапустили, а потом на статистику ошибок поглядели и что-то поправили, или даже оставили так
Потом, правда, Алиса кладёт весь NTP, с диска C: всё удаляется, и так далее, но это ничего страшного, просто посмотрим статистику ошибок и что-то поправим.
А если не секрет, зачем вообще с таким подходом тесты писать? Написали код, запустили-потыкали пару раз, вроде работает ⇒ деплоим в прод. Если что-то навернётся — тоже перезапустили, статистика ошибок, оставили так.
ednersky
01.01.2025 10:25тесты писать нужно для того, чтобы быстрее приходить к нужному результату
с тестами скорость разработки где-то вдвое-втрое выше, чем без оных
увы, это не все понимают
а если проекту несколько лет, то тесты ускоряют разработку более чем на порядок
IUIUIUIUIUIUIUI
01.01.2025 10:25Как они помогают прийти к нужному результату? Они только мешают, их обновлять надо, поддерживать, все дела. А так нафигачил и го в прод. Я вот на одном проекте без тестов фигачил и очень быстро всё сделал, триллионы долларов заработали.
Что не так?
ednersky
01.01.2025 10:25Что не так?
внесение изменений в код "не так".
в большом проекте есть множество кода А. Новичок-програмист работает над подмножеством B, а другой его сосед над подмножеством C. Каждый из них запуская свои тесты убеждается, что у него лично всё работает. А потом система CI запускает ВСЕ тесты и показывает им, что первый не помешал/повредил второму и наоборот.
Вашу систему вы писали в одиночку, поэтому такое на начальном этапе работало.
Zenitchik
01.01.2025 10:25Даже когда систему пишешь в одиночку, чертовски полезно зафиксировать поведение в тестах, чтобы потом иметь возможность автоматизированного контроля, изменилось оно или нет.
IUIUIUIUIUIUIUI
01.01.2025 10:25Абсолютно та же логика работает с типами.
И обратно, абсолютно так же все пока что упомянутые вами возражения против типизации работают и как возражения против тестов. И экранов кода там больше, и бро из соседнего комментария с MVP тестами не пользовался.
ednersky
01.01.2025 10:25Неа, типы не заменяют и 1% функциональности тестов. Но при этом и тесты и типы приносят оверхед (ваше паясняченье выше - именно о нём, об оверхеде).
Бесплатных фич не бывают.
и вот если с тестами профит от них перекрывает расходы на них, то с типами всё наоборот:
читабельность кода радикально понижается
количество кода радикально растёт
при этом количество проблем, которые решаются типами мало
а типы начинают мешать таким простым задачам как "написать функцию, возвращающую сумму двух чисел" - приходится геморроиться с дженериками и прочей ненужной магией
redbeardster
01.01.2025 10:25Большой молодец, пишите еще, спасибо! Lean4 нравится тем, что готов к употреблению как ЯП с завтипами, а как пруф-ассистант мила Изабелла: AFP и seL4 весьма хороши и полезны
kciray Автор
01.01.2025 10:25Слышал про seL4, крутая штука. У coq правда есть аналогичный проект - CertiKOS
Lean4 нравится тем, что готов к употреблению как ЯП с завтипами
Интересно, спасибо. У Coq есть такая проблема, что на нем самом не очень получится приложения разработать
ermouth
01.01.2025 10:25Она (HoTT) настолько не готова, что даже в начале учебника по гомотопической теории типов написано, что теория в процессе изменений и все может поменяться
Книжке много лет, Воеводский умер, к сожалению, и движения там и правда особо не наблюдается. Тем не менее, прочитать книжку стóит – горизонты понимания что такое тип она точно расширит, особенно если у вас геометрическая/топологическая интуиция прокачана.
По применимости – открытый вопрос, вот недавнее обсуждение https://mathoverflow.net/questions/480656/hott-for-the-working-mathematician-especially-the-homotopy-geometer-what-is
Пиано
Сейчас так уже не принято, чаще пишут Пеано.
kciray Автор
01.01.2025 10:25у вас геометрическая/топологическая интуиция прокачана
Ох не люблю я эту геометрическую интуицию, всегда ее ненавидел еще со школы... Бррррр
Спасибо за замечание, мб прочитать первые пару-тройку глав действительно стоит, прочтение книги занимает в 4-5 раз меньше усилий, чем прочтение + выполнение упражнений + их формализация
IUIUIUIUIUIUIUI
01.01.2025 10:25К сожалению (я тоже не люблю топологию), похоже, без этого никуда. Лучше всего взять какую-нибудь лайтовую книжку по топологии и просто по ней пробежаться-прорешать задачи, чтобы развить топологическую интуицию. Introduction to Topology: Pure and Applied, например, меня порадовала (и там в конце главы с прикольными прикладными задачами, что хороший отдых от всей этой фундаментальной абстрактщины). Только заранее рекомендую открыть её errata и держать рядом — там есть ошибки и опечатки.
NeoCode
01.01.2025 10:25Кстати большинство (и я в том числе) проголосовали за постижение Тайн Мироздания:)
Увы, в моем ВУЗе все эти основания математики не изучали (из математики была линейная алгебра, матан, дискретка, тервер, численные методы). Но тема очень интересная, всегда хотелось погрузиться в нее поглубже.
Поэтому вопрос к тем кто глубоко в теме: что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
kciray Автор
01.01.2025 10:25Кстати большинство (и я в том числе) проголосовали за постижение Тайн Мироздания:)
Вот тут для меня была неожиданность, действительно этот пункт оказался очень популярен и сейчас лидирует. Мне тоже интересно =) Но ML в большем приоритете у меня
Увы, в моем ВУЗе все эти основания математики не изучали
А у кого их изучали?) Ладно, у нас был профессор Лагодинский, который давал математическую логику довольно глубоко. Но не конструктивным путем (через таблицы истинности) и без опоры на формализацию и теорем-пруверы.
что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
Andy_U
01.01.2025 10:25Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
Вот не поверю, что можно математически вывести отстутствие магнитных зарядов в природе.
NeoCode
01.01.2025 10:25Но ML в большем приоритете у меня
Непонятно при чем тут ML. Это же по сути самые обычные (и вообще говоря приближенные) вычисления, но в ОЧЕНЬ большом количестве. Никакими основаниями математики там и не пахнет (ИМХО конечно), это просто почти школьная математика, а весь вау-эффект достигается за счет перехода количества в качество.
Вот здесь статья о реверс-инжиниринге простейшей нейросети, которую обучили для сложения двоичных чисел. Ожидалось что она воспроизведет внутри себя что-то вроде "двоичного сумматора", применяемого во всех микропроцессорах, по оказалось что сеть пошла по принципиально иному пути... И в некотором смысле этот другой путь гораздо ближе к природе, чем двоичные сумматоры.
IUIUIUIUIUIUIUI
01.01.2025 10:25Поэтому вопрос к тем кто глубоко в теме: что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Ничего не могу сказать, к сожалению (но я ненастоящий сварщик).
Математика — это просто наука о том, как обращаться с закорючками по правилам, а основания математики — это кусочек этой науки, в котором закорючками являются правила обращения с другими закорючками.
Насколько я могу судить, физикам вся эта глубокая муть не нужна: они счастливо работают с наивной математикой по большому счёту 19-го века, и им норм. Я по разным причинам наиболее интересуюсь теорией топосов, и если смотреть на работы теоретических физиков по их применению, например, в качестве оснований (а не языка для выражения), то там дело ограничивается очень узким множеством статей вроде таких — https://arxiv.org/pdf/2110.06793 или https://arxiv.org/pdf/1106.5660 , у которых цитирований по десятку-другому максимум (то есть, физикам эта тема не очень интересна, а ИМХО если уж что из оснований и может претендовать на прорывные результаты, так это топосы).
И, например, не придумано экспериментов, способных фальсифицировать наличие или отсутствие C в ZF+C-аксиоматике нашего мира (я склонен считать, что парадокс Банаха-Тарского ближе к нереализуемым бесконечностям, чем к отсутствию C, и если для вас он что-то опровергает, то в вашем мире не должно существовать и, скажем, всего множества вещественных чисел), или отличить ZF+C от других аксиоматик, или сказать, описывается наш мир классической или конструктивной логикой.
Но это всё, конечно, не значит, что таких экспериментов не может быть. И даже если вдруг окажется, что в нашем мире C нет, или логика классическая, то это не делает ZF+C и классическую логику более плохой математикой.
Основания математики по определению замкнуты на себя самих.
kozlyuk
01.01.2025 10:25А теперь поговорим о списке практических применений фундаментальной математики.
Извините за "диагноз по фотографии", но по-моему вы просто искренне и бескорыстно тащитесь от всего, что написано до приведенной фразы. И это прекрасно и не нуждается в притягивании за уши применений. Целую цивилизацию отгрохали, чтобы можно делать то, что хочется, а не только необходимое зачем-нибудь.
Сомнительны применения, связанные со статистикой и линейной алгеброй. Абстракция — мощнейший инструмент мышления. Скорее всего, принять на веру те начала мат. стиатистики и т. п., которые фундаментальной математикой можно вывести, ничуть не помешает изучению, зато позволит [вашим конкурентам] начать его раньше.
Формализация ПО и баз данных для обычного бизнеса запретительно дорога. Но! Рекомендую посмотреть в сторону безопасных (secure, safe) и доверенных систем (trustworthy). Именно там востребованы строгие доказательства и то, чтобы поменьше принимать за данность.
Раз интересна 3D-графика, рядом есть более серьезное направление — вычислительные методы. С точки зрения работы реального ИИ они, скорее всего, не менее релевантны, чем линейная алгебра, да и в 3D-графике о погрешностях надо думать.
Глубоко понять, как устроен реальный мир на низком уровне.
учился в аспирантуре [...], сдал академический минимум
Вы же сдавали философию...
kciray Автор
01.01.2025 10:25ничуть не помешает изучению, зато позволит [вашим конкурентам] начать его раньше.
Да у нас вроде нету спешки проходить настолько базовые предметы. Они же проходятся один раз и на всю жизнь, и лучше это сделать более качественно и глубоко (на мой взгляд). Еще можно разбить на 2 этапа, в первом этапе вы проходите эти предметы по какому-нибудь поверхностному курсу, а потом возвращаетесь и проходите по более глубокому курсу с более глубоким покрытием фундамента. Собственно, я пошел именно таким путем почти по всем предметам.
Вы же сдавали философию...
Так вот, как раз философия и заставляет двигаться глубже. В общих чертах этот пункт я понимаю уже давно, уровни организации материи всякие (стандартная модель -> физика -> химия -> биология -> астрофизика -> теория большого взрыва). Но хочется больше деталей и формальной верификации, так как очень много дыр в понимании.
Edwward
01.01.2025 10:25Что бы быть чемпионом формулы 1 , обязательно знать все процессы происходящие в двигателе, на фундаментальном уровне?
И не обязательно знать математику на таком "царском", уровне, как Вы описываете, что бы быть хорошим инженером в ml. Достаточно базового , университетского уровня.
А еще важней, для програмиста/ разработчика, уметь понимать специфику бизнес задач, умение "нырнуть" в предметную область.
kciray Автор
01.01.2025 10:25что бы быть хорошим програмистом
Ну это очень мутное понятие, каждый его по-разному интерпретирует. Как вы формально определите критерии "хорошего программиста"?
Для некоторых хороший программист - это тот, кто просто умеет писать чистый код. Для других - тот, кто умеет нужные библиотеки и фреймворки подключать\соединять. Для третьих это тот, кто удобен бизнесу и понимает требования\решает проблемы в адекватный срок. Для четвертых это тот, кто хорошо знает алгоритмы и структуры данных, сердце компьютерных наук.
Все это я уже проходил и хочется двигаться дальше.
RikkiMongoose
01.01.2025 10:25Судя по количеству компиляторов и линтеров, написанных на Coq (их целых 0), это определение нуждается в переопределении
KReal
01.01.2025 10:25Что бы быть чемпионом формулы 1 , обязательно знать все процессы происходящие в двигателе, на фундаментальном уровне?
Сильно подозреваю, что таки знают.
RikkiMongoose
01.01.2025 10:25Про подобную "французскую математику" очень остроумно рассказывал покойный Арнольд. По моему опыту общения с современными французскими промышленными инженерами, с таким подходом непостижимая математика начинает где-то в таблице умножения.
Дальше цитируем Арнольда:
Оказывается, нуль - положительное число. Действительно, для Бурбаки все общие понятия важнее их частных случаев, поэтому все нестрогие неравенства являются фундаментальными, а строгие - маловажными специальными случаями, примерами. В соответствии с этим во Франции слово "больше" в математике означает то, что мы называем "больше или равно". Например, каждое вещественное число больше самого себя, а значит, нуль больше нуля и, следовательно, положителен!
...
Кроме положительности нуля, то же рассуждение устанавливает и его отрицательность (ибо нуль меньше нуля по французско-бурбакистской терминологии). Мои коллеги и ученики разъяснили мне, что нуль входит также и в множество неположительных чисел, а заодно и в множество неотрицательных чисел. Но Серр, кроме указанных неравенств, доказал еще одно свойство нуля: он оказывается вдобавок числом натуральным.
...В уже упомянутом руководстве для первокурсников все это используется для определения факториала. Вот это определение: во-первых, 0! = 1; во-вторых, для любого натурального числа n имеет место равенство (n + 1)! = (n + 1)n!.
Если не знать, что нуль - натуральное число, то ни одного факториала невозможно ни определить, ни понять, ни вычислить. Кстати, обычное определение n! = 1• 2 • ... • n, во-первых, не фигурирует в этом тексте нигде, и, во-вторых, считается ошибочным. А именно: во-первых, участвующие в этом определении три точки не определены, а во-вторых, определение не годится ни для n = 0, ни для n = 1.Раз уж я стал разбирать это руководство, процитирую из него еще одно место. Речь идет теперь об определении науки математики, чтобы студенты знали, что им предстоит:
"Математика есть наука о доказательствах, доказательства это цепочки импликаций: (из А вытекает В, из В вытекает С) - цепочка; вывод: доказано, что из А вытекает С. Итак, самое главное - понять, что такое одна импликация. Вот ее определение. Пусть А и В - два произвольных высказывания. Если оба они верны, то говорят, что из А вытекает В".
На мой непросвещенный взгляд, такая точка зрения на импликации (а следовательно, и на доказательства, и на математику) - чистое мракобесие. При таком определении из того, что дважды два четыре, следует, что Земля вращается вокруг Солнца.Студента, понимающего выводы и доказательства подобным образом, уже бесполезно учить какой-либо естественной науке: мракобесие уничтожает естествознание как таковое. По этой мракобесной логике Галилея поделом наказывали: он ведь говорил о своих доказательствах вращения Земли и других подобных фактов совсем в другом смысле.
...
Из других бурбакистских принципов, упомянутых Серром, назову еще утверждение о полной независимости математики от физики. В одном своем письме ко мне Серр уже заявил, что "у математики и физики нет ничего общего", но он добавил тогда, что "не станет публиковать этого утверждения, потому что нам, математикам, не следует высказываться по философским вопросам, ибо самые лучшие из нас способны высказать здесь совершеннейшую чушь".
...
Антифизические идеи в математике давно популяризируются самыми разными ее представителями. Г. Харди, например, объяснял (в недавно изданной по-русски "Апологии математика") слова Гаусса "теория чисел - королева математики" сходством теории чисел с королевой: это сходство заключается, согласно Харди, в полной бесполезности обеих.
...
В середине двадцатого века была предпринята попытка разделить математику и физику. Последствия оказались катастрофическими. Выросли целые поколения математиков, незнакомых с половиной своей науки и, естественно, не имеющих никакого представления ни о каких других науках. Они начали учить своей уродливой схоластической псевдоматематике сначала студентов, а потом и школьников (забыв о предупреждении Харди, что для уродливой математики нет постоянного места под Солнцем).Поскольку ни для преподавания, ни для приложений в каких-либо других науках схоластическая, отрезанная от физики, математика не приспособлена, результатом оказалась всеобщая ненависть к математикам — и со стороны несчастных школьников (некоторые из которых со временем стали министрами), и со стороны пользователей.
Уродливое здание, построенное замученными комплексом неполноценности математиками-недоучками, не сумевшими своевременно познакомиться с физикой, напоминает стройную аксиоматическую теорию нечётных чисел. Ясно, что такую теорию можно создать и заставить учеников восхищаться совершенством и внутренней непротиворечивостью возникающей структуры (в которой определена, например, сумма нечётного числа слагаемых и произведение любого числа сомножителей). Чётные же числа с этой сектантской точки зрения можно либо объявить ересью, либо со временем ввести в теорию, пополнив её (уступая потребностям физики и реального мира) некоторыми «идеальными» объектами.
К сожалению, именно подобное уродливое извращённое построение математики господствовало в преподавании математики в течение десятилетий. Возникнув первоначально во Франции, это извращение быстро распространилось на обучение основам математики сперва студентов, а потом и школьников всех специальностей (сперва во Франции, а потом и в других странах, включая Россию).
Ученик французской начальной школы на вопрос «сколько будет 2+3» ответил: «3+2, так как сложение коммутативно». Он не знал, чему равна эта сумма, и даже не понимал, о чем его спрашивают!
Другой французский школьник (на мой взгляд, вполне разумный) определил математику так: «там есть квадрат, но это нужно ещё доказать».
По моему преподавательскому опыту во Франции, представление о математике у студентов (вплоть даже до обучающихся математике в École Normale Supérieure — этих явно неглупых, но изуродованных ребят мне жалко больше всего) — столь же убого, как у этого школьника.
...
Попытки создания «чистой» дедуктивно-аксиоматической математики привели к отказу от обычной в физике схемы (наблюдение — модель — исследование модели — выводы — проверка наблюдениями) и замена её схемой: определение — теорема — доказательство. Понять немотивированное определение невозможно, но это не останавливает преступных алгебраистов-аксиоматизаторов. Например, они были бы готовы определить произведение натуральных чисел при помощи правила умножения «столбиком». Коммутативность умножения становится при этом трудно доказываемой, но все же выводимой из аксиом теоремой. Эту теорему и её доказательство можно затем заставить учить несчастных студентов (с целью повысить авторитет как самой науки, так и обучающих ей лиц). Понятно, что ни такие определения, ни такие доказательства, ни для целей преподавания, ни для практической деятельности, ничего, кроме вреда, принести не могут.
...
Если математики не обучаются сами, то потребители, сохранившие как нужду в современной в лучшем смысле слова математической теории, так и свойственный каждому здравомыслящему человеку иммунитет к бесполезной аксиоматической болтовне, в конце концов откажутся от услуг схоластов-недоучек и в университетах, и в школах.
Zenitchik
01.01.2025 10:25Много пропаганды, мало сути.
RikkiMongoose
01.01.2025 10:25Суть хорошо изложена в исходной статье. Математика исторически развивалась сначала параллельно землемерию (геометрия), а потом физике (интегральное счисление для ньютоновой, тензорный анализ для ОТО). Вся эта формализация (которую Фреге делал - не доделал, потом Рассел и Уайтхед делали - не доделали, потом группа Бурбаки делала - не доделала, теперь вот Воеводский делал - не доделал) не просто избыточно сложна и по большому счёту бесполезна, но ещё и совершенно непонятна посторонним. Отсюда сектантский апломб адептов, потому что адекватному человеку совершенно непонятно, зачем погружаться в это бесконечное определение определений, абстракции над ещё большими абстракциями и сомнительные утверждения, которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Как быть с исследованиями Гёделя о том, что невыводимые теоремы всё равно существуют и их бесконечно много? С работами Лакотоса (который показал, что доказательство - по большому счёту конструкт и результат консенсуса)? С математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих (игра Жизнь так устроена, и тот же Стивен Вольфрам вообще считает, что в этом и есть будущее математики)?
А никак. Этому не учили.
IUIUIUIUIUIUIUI
01.01.2025 10:25не просто избыточно сложна и по большому счёту бесполезна, но ещё и совершенно непонятна посторонним. Отсюда сектантский апломб адептов, потому что адекватному человеку совершенно непонятно, зачем погружаться в это бесконечное определение определений, абстракции над ещё большими абстракциями и сомнительные утверждения, которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Это, вообще говоря, и к обычной, прикладной математике применимо как псевдоаргумент. А то придумали там какие-то парадоксы дней рождения, тоже мне. 183 человека нужно, чтобы вероятность совпадения днюхи была ½, и всё тут.
Как быть с исследованиями Гёделя о том, что невыводимые теоремы всё равно существуют и их бесконечно много?
Так с ними и быть. Не понимаю проблем.
С работами Лакотоса (который показал, что доказательство - по большому счёту конструкт и результат консенсуса)?
Консенсуально доказали с пацанами, что от вышек 5G случается ВИЧ, как с этим быть?
И «183 человека» тоже консенсуально объявили правильным ответом.Надо закопать конкретно эти работы Лакатоса.
С математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих
А в чём с ними проблема? Берёте и вычисляете.
(игра Жизнь так устроена, и тот же Стивен Вольфрам вообще считает, что в этом и есть будущее математики)?
Если говорить о ненужности оснований математики могут разные люди с разными взглядами (включая, скажем, прикладных математиков, которым это всё не нужно для их работы в прямом смысле), то при этом упоминать Вольфрама с его new kind of science в положительном ключе могут только фоменковцы от математики.
RikkiMongoose
01.01.2025 10:25к обычной, прикладной математике применимо как псевдоаргумент.Как раз к прикладной математике оно отлично применимо. Многие математические объекты вроде комплексных чисел как раз и появились для описания моделей природных процессов.
Так с ними и быть. Не понимаю проблем.Действительно: существует бесконечное количество истинных теорем, которые невозможно доказать с помощью системы для доказательства теорем. Казалось бы, что тут может быть не так?
Надо закопать конкретно эти работы Лакатоса.Для начала вам было полезно их хотя бы прочитать.
Достаточно начать с "Доказательства и опровержения". 152 страницы последовательно разворачивается история доказательства теоремы Эйлера для многогранников. В принципе, доказал её ещё Эйлер - но каждое новое поколение математиков добавляет уточнения и конца этому процессу не видно.
На какой же странице этой книги теорема Эйлера становится доказанной? На 5-ой (где приведено доказательство Эйлера)? На 152 - где признаётся, что на момент написания книги "она верна для многогранников, топологически эквивалентных сфере"? Но топология продолжает развиваться и скорее всего, и это определение неточно.
А в чём с ними проблема? Берёте и вычисляете.В том, что из аксиом, без вычислений, это значение получить нельзя.
при этом упоминать Вольфрама с его new kind of science в положительном ключе могут только фоменковцы от математикиНу, у Вольфрама есть заслуги перед наукой - его Mathematica имеет широчайшее применение.
Где применяются мощнейшие исследования Вопенки и Воеводоского? Нигде. Возникает ощущение, что их адепты просто больше ничего не умеют.
IUIUIUIUIUIUIUI
01.01.2025 10:25Как раз к прикладной математике оно отлично применимо. Многие математические объекты вроде комплексных чисел как раз и появились для описания моделей природных процессов.
И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
По-моему, это просто какое-то переусложнение ради переусложнения. Например, не зря великий Декарт называл их «воображаемыми» числами, а Гаусс сомневался в осмысленности их метафизики.
И это мы ещё всяких греков и иррациональные числа не вспоминали.
Действительно: существует бесконечное количество истинных теорем, которые невозможно доказать с помощью системы для доказательства теорем. Казалось бы, что тут может быть не так?
Их вообще невозможно доказать (во вкладываемом вами смысле), даже ручкой на бумажке, пруверы тут ни при чём.
Но таки да, что же тут не так? Давайте, доводите мысли до конца, чтобы не пришлось за вас додумывать.
Для начала вам было полезно их хотя бы прочитать.
Так я их читал.
Как там дела с количеством людей для парадокса дня рождения? Вы согласны, что нужно 183 человека? Если не согласны, то вон Росатый стоит, он в 90-ые очень авторитетным авторитетом был, и сейчас быстро вас убедит.
В том, что из аксиом, без вычислений, это значение получить нельзя.
Не понял, откуда тут взялась дихотомия между аксиомами и вычислениями?
Ну, у Вольфрама есть заслуги перед наукой - его Mathematica имеет широчайшее применение.
У Фоменко тоже есть заслуги в математике, но это не делает его авторитетом в истории. Точно так же с Вольфрамом: заслуги в софтварной инженерии не делают его авторитетом в основаниях математики.
RikkiMongoose
01.01.2025 10:25И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
Переменный ток, который это всё освещает? Почти вся теория электрических цепей описывается комплексными числами.
Вот ещё пара примеров из Арнольда:
Когда я учился на первом курсе мех.-мата МГУ, лекции по анализу читал теоретико-множественный тополог Л. А. Тумаркин, добросовестно пересказывающий старый классический курс анализа французского образца, типа Гурса. Он сообщил нам, что интегралы от рациональных функций вдоль алгебраической кривой берутся, если соответствующая риманова поверхность — сфера, и, вообще говоря, не берутся, если род её выше, и что для сферичности достаточно существования на кривой данной степени достаточно большого числа двойных точек (вынуждающих кривую быть уникурсальной: её вещественные точки можно нарисовать на проективной плоскости единым росчерком пера).
Эти факты настолько поражают воображение, что (даже сообщённые без всяких доказательств) дают большее и более правильное понятие о современной математике, чем целые тома трактата Бурбаки. Ведь мы узнаем здесь о существовании замечательной связи между вещами на вид совершенно различными: существованием явного выражения для интегралов и топологией соответствующей римановой поверхности, с одной стороны, а с другой стороны — между числом двойных точек и родом соответствующей римановой поверхности, проявляющемся вдобавок в вещественной области в виде уникурсальности.
Уже Якоби заметил, как самое восхитительное свойство математики, что в ней одна и та же функция управляет и представлениями целого числа в виде суммы четырёх квадратов, и истинным движением маятника.
Эти открытия связей между разнородными математическими объектами можно сравнить с открытием связи электричества и магнетизма в физике или сходства восточного берега Америки с западным берегом Африки в геологии.
Понять коммутативность умножения можно, только либо пересчитывая выстроенных солдат по рядам и по шеренгам, либо вычисляя двумя способами площадь прямоугольника. Попытки обойтись без этого вмешательства физики и реальности в математику — сектанство и изоляционизм, разрушающие образ математики как полезной человеческой деятельности в глазах всех разумных людей.
Определитель матрицы — это (ориентированный) объём параллелепипеда, рёбра которого — её столбцы. Если сообщить студентам эту тайну (тщательно скрываемую в выхолощенном алгебраическом преподавании), то вся теория детерминантов становится понятной главой теории полилинейных форм. Если же определять детерминанты иначе, то у каждого разумного человека на всю жизнь останется отвращение и к определителям, и к якобианам, и к теореме о неявной функции.
Что такое группа? Алгебраисты учат, будто это множество с двумя операциями, удовлетворяющими куче легко забываемых аксиом. Это определение вызывает естественный протест: зачем разумному человеку такие пары операций? «Да пропади она пропадом, эта математика» — заключает студент (делающийся в будущем, возможно, министром науки).
Положение становится совершенно иным, если начать не с группы, а с понятия преобразования (взаимно-однозначного отображения множества в себя), как это и было исторически. Набор преобразований какого-либо множества называется группой, если вместе с любыми двумя преобразованиями он содержит результат их последовательного применения, а вместе с каждым преобразованием — обратное преобразование.
Их вообще невозможно доказать (во вкладываемом вами смысле), даже ручкой на бумажке, пруверы тут ни при чём.
Снова Арнольд:
"«Тонкий яд математического образования» (по выражению Ф. Клейна) для физика состоит именно в том, что абсолютизируемая модель отрывается от реальности и перестаёт с нею сравниваться. Вот самый простой пример: математика учит нас, что решение уравнения Мальтуса dx/dt = x однозначно определяется начальными условиями (т.е. что соответствующие интегральные кривые на плоскости (t, x) не пересекают друг друга). Этот вывод математической модели имеет мало отношения к реальности. Компьютерный эксперимент показывает, что все эти интегральные кривые имеют общие точки на отрицательной полуоси t. И действительно, скажем, кривые с начальными условиями x(0) = 0 и x(0) = 1 при t = –10 практически пересекаются, а при t = –100 между ними нельзя вставить и атома. Свойства пространства на столь малых расстояниях вовсе не описываются евклидовой геометрией. Применение теоремы единственности в этой ситуации — явное превышение точности модели. При практическом применении модели это надо иметь в виду, иначе можно столкнуться с серьёзными неприятностями."
Так я их читал.
Обманывать нехорошо.
Как там дела с количеством людей для парадокса дня рождения? Вы согласны, что нужно 183 человека?
Вы путаете недоказуемость с контринтуитивностью. Можно (и нетрудно, те же диаграммы Эйлера в помощь) вывести основные формулы теории вероятности, подставить исходные числа и подсчитать. "парадокс заключается лишь в различиях между интуитивным восприятием ситуации человеком и результатами математического расчёта."
Не понял, откуда тут взялась дихотомия между аксиомами и вычислениями?
Ну как же, логические операции не позволяют ничего вычислять. Они позволяют только определить тавтологию.
То есть они могут определить, что если у нас есть состояние b, то применяя операцию F мы получим состояние b. F(a) = b
Но как доказать, что состояние x получается из a путём конечного количества применений функции F? Только выстроив цепочку преобразований, т.е. перебором.
У Фоменко тоже есть заслуги в математике, но это не делает его авторитетом в истории. Точно так же с Вольфрамом: заслуги в софтварной инженерии не делают его авторитетом в основаниях математики.
В том и дело, что у new kind of science есть практические результаты - вся книга их ему посвящена.
Какие результаты у Вопенки с Воеводским? «Там есть квадрат, но это нужно ещё доказать».
IUIUIUIUIUIUIUI
01.01.2025 10:25Вы упустили уточнение вопроса про невыводимые теоремы. Вопрос снят, или вы решили проигнорировать эту ветвь?
Переменный ток, который это всё освещает? Почти вся теория электрических цепей описывается комплексными числами.
Считал в школе задачки на переменный ток без комплексных чисел, нормально жил. Утверждаю, что это всё ненужные, воображаемые вещи.
Обманывать нехорошо.
Знаю, поэтому и не обманываю.
Вы путаете недоказуемость с контринтуитивностью.
Нет. Я вам наглядно показываю, насколько бредово определение доказательства как конструкта и социального феномена.
Можно (и нетрудно, те же диаграммы Эйлера в помощь) вывести основные формулы теории вероятности
Ненужное переусложнение ради интеллектуальной мастурбации, разве нет?
Ну как же, логические операции не позволяют ничего вычислять. Они позволяют только определить тавтологию.
Вычисление в данном случае — это приведение терма в нормальную форму, в чём вопрос-то? Или вы застряли где-то на уровне исчисления высказываний?
Но как доказать, что состояние x получается из a путём конечного количества применений функции F?
Конечного, но не заданного наперёд? Это уже совсем другой вопрос, с которым у вас будут проблемы даже в вашем подходе.
В том и дело, что у new kind of science есть практические результаты - вся книга их ему посвящена.
Нет, он там занимается в основном глубоким философствованием о сути бытия, и о том, что экспериментальная проверка вселенной-как-клеточного-автомата может быть выполнена, если упрощать. Практических результатов там абсолютный ноль.
Я был бы готов записать тьюринг-полноту правила 110 в практические результаты, конечно, но, учитывая вашу позицию, не уверен, что это будет для вас сколь угодно практичным.
RikkiMongoose
01.01.2025 10:25Я не могу тратить силы на объяснение, почему у вас всё никак не получается пошутить. Даже Лакотос (которого вы не читали), понятный неглупому старшекласснику, для вас слишком сложный.
Поэтому вот вам вопрос на вашем уровне:
Комплексные числа позволяют достаточно просто описать и решить многие задачи электродинамики (более сложные, чем те, которые вы решали в школе).
Формулы теории вероятности позволяют достаточно просто подсчитать вероятность совпадения дня рождений (что невозможно сделать наугад).
Клеточные автоматы очень активно применяются в моделировании физических процессов ещё годов с 1970-х. Они быстрее и проще аналогов.
Даже Тьюринг свою модель машины строил как раз для того, чтобы сделать более наглядным и понятным решение задач, которые другим способом требовали бы огромных вычислений, в которых было бы невозможно разобраться.
Какие физические (или вычислительные) задачи позволяет короче и яснее решить вся это болтовня об основаниях математики, в которой уже 100 лет назад во всём мире могли разобраться 12 человек? Ну кроме задачи защиты ещё одной кандидатской диссертации.
IUIUIUIUIUIUIUI
01.01.2025 10:25Я не могу тратить силы на объяснение, почему у вас всё никак не получается пошутить.
Неужели нужно так много сил на высказывание «потому что пошутить нет цели»? Ведь у меня действительно нет цели пошутить, а есть цель показать, что ваш метод рассуждений приводит к очевидно бредовым результатам в более близким вам областям.
Впрочем, это требует от вас некоторых навыков абстрактного мышления, и, возможно, моя ошибка — априори ожидать этих навыков.
Комплексные числа позволяют достаточно просто описать и решить многие задачи электродинамики (более сложные, чем те, которые вы решали в школе).
Отвечу цитатой великих:
«Вся эта формализация [...] совершенно непонятна посторонним. Адекватному человеку совершенно непонятно, зачем погружаться во взятие интегралов вычетами, чтобы просто рассчитать цепь.»
И правда, кстати, посторонним относительно электродинамики формализация цепей через комплексные выражения совершенно непонятна.
Формулы теории вероятности позволяют достаточно просто подсчитать вероятность совпадения дня рождений (что невозможно сделать наугад).
Отвечу цитатой великих:
Вся эта формализация [...] совершенно непонятна посторонним. Адекватному человеку совершенно непонятно, зачем погружаться в эти формализации и разложения Хана ради конечно аддитивных сигма-алгебр, чтобы просто посчитать дни рождения.
И правда, кстати, ведь если бы это было понятно посторонним, то парадокс дней рождения не был бы парадоксом.
Клеточные автоматы очень активно применяются в моделировании физических процессов ещё годов с 1970-х. Они быстрее и проще аналогов.
Отвечу ци… пажжите, с 1970-х? Вольфрам свой интерес к клеточным автоматам начал с 80-х (зайдя с козырей и патентования правила 110 — очень научный подход). Вы походу сами себя переспорили.
И, кстати, с 50-х, ещё с фон Неймана.
Даже Тьюринг свою модель машины строил как раз для того, чтобы сделать более наглядным и понятным решение задач, которые другим способом требовали бы огромных вычислений, в которых было бы невозможно разобраться.
Такое сказать может только человек, знакомый с машиной Тьюринга только по первому абзацу википедии. Формализм Тьюринга не делает ничего ни понятным, ни наглядным, потому что программирование МТ — это ад.
Тоже вычёркиваем из практических применений.
Какие физические (или вычислительные) задачи позволяет короче и яснее решить вся это болтовня об основаниях математики, в которой уже 100 лет назад во всём мире могли разобраться 12 человек?
Мне даже далеко ходить не надо — теоркат даёт основания для Giry monad, что даёт вычислительные основания для сэмплирования и байесовского вывода в том же monad-bayes, которой я пользуюсь вот прямо сейчас.
Но давайте с другой стороны. Какие практические результаты дала теоретическая физика за последние, скажем, 50 лет? Какие продвижения были в вычислительной математике? Рунге-Кутте лет 120. Закрываем физику и математику и раздаём освободившиеся деньги бездомным?
RikkiMongoose
01.01.2025 10:25зачем погружаться в эти формализации и разложения Хана ради конечно аддитивных сигма-алгебр, чтобы просто посчитать дни рождения.
Действительно, аддитивных сигма-алгебр тут не нужно, достаточно оснований математике, известных ещё древним шумерам.
Вероятность того, что у одного день рождения не совпадёт с днем рождения другого человека, равна 1 - 1/365. Дальше проверяем по несовпадение третьего и т.д. По индукции легко выводится общая формула.
Зачем здесь разложение Хана? Зачем алгебры подмножеств? А 2 + 2 сложить можно, если не знаешь, что ноль больше самого себя?
Формализм Тьюринга не делает ничего ни понятным, ни наглядным, потому что программирование МТ — это ад.
Если бы вы прочли исходную статью Тьюринга, то убедились бы, что никакого "программирование" там и нет.
теоркат даёт основания для Giry monad, что даёт вычислительные основания для сэмплирования и байесовского вывода в том же monad-bayes, которой я пользуюсь вот прямо сейчас.
С тем же успехом можно сказать, что до работ Пеано люди не умели считать, потому что не было оснований для арифметики.
Хотя вот когда французов начали учить по принципу "надо просто выучить определения" - проблемы начались уже и с арифметикой...
Основания могут быть очень разными, на то они и основания, чтобы доказывать то, что уже есть. Да вот только Giry monad появились задолго до формализации - а именно, в 1962, как метод решений конкретных задач: https://ncatlab.org/nlab/show/Giry+monad#history
Прямо так и написано:
I’d like to say that the idea of the category of probabilistic mappings, the document corresponding to that was not part of a seminar, as some of the circulations say, essentially it was the document submitted to the arms control and disarmament agency after suitable checking that the Pentagon didn’t disagree with it. Because of the fact that for arms control agencies as a side responsibility the forming of arms control agreements and part of these agreements must involve agreed upon protocols of verification. So the idea of that paper did not provide such protocols, but it purported to provide reasonable framework within which such protocol can be formulated.
IUIUIUIUIUIUIUI
01.01.2025 10:25Действительно, аддитивных сигма-алгебр тут не нужно, достаточно оснований математике, известных ещё древним шумерам.
Ура! Осталось понять, что и вам не обязательно доводить всё до абсурда в описании оснований математики.
Вероятность того, что у одного день рождения не совпадёт с днем рождения другого человека, равна 1 - 1/365. Дальше проверяем по несовпадение третьего и т.д. По индукции легко выводится общая формула.
Фигня какая-то, да и индукция пошла, а это уже основания математики. Не могу в этом разобраться, и все мои знакомые не могут. Придумки академиков, чтобы написать ещё один диссер.
У меня в «5В» классе вот меньше 183 человек, и дни рожденья ни у кого не совпадают. В соседнем «5Г» то же.
Если бы вы прочли исходную статью Тьюринга, то убедились бы, что никакого "программирование" там и нет.
Вы ранее написали:
строил как раз для того, чтобы сделать более наглядным и понятным решение задач
Исходная статья в этой формулировке не является ни необходимым, ни достаточным источником.
Или давайте по-другому: какие задачи стали более наглядны и понятны с машиной Тьюринга?
С тем же успехом можно сказать, что до работ Пеано люди не умели считать, потому что не было оснований для арифметики.
До работ Пеано (а также Пресбургера, и всех прочих, кто анализировал эту область) не было понятно, какие задачи имеет смысл пытаться решать, а какие — нет (потому что арифметика Пеано неразрешима, а Пресбургера — разрешима).
Да вот только Giry monad появились задолго до формализации
Это и есть формализация. Она появилась задолго до самой себя?
piton_nsk
01.01.2025 10:25И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
Риторический вопрос - разве можно увидеть даже не отрицательные, а обычные натуральные числа? Вот у меня на столе сейчас лежит один брелок от автосигналки и 3 батарейки 3А. Я их вижу и могу потрогать, а где можно потрогать число три или единицу?
IUIUIUIUIUIUIUI
01.01.2025 10:25Ну вы их посчитали, хотя бы, и можно сказать, что число «три» — это такой же концепт и так же относится к трём батарейкам, как концепт «собака» относится к вашей конкретной Жучке.
А вот отрицательные числа уже тоже проделки дьявола.
piton_nsk
01.01.2025 10:25число «три» — это такой же концепт
Какая-никакая, а все же абстракция, руками не потрогаешь.
IUIUIUIUIUIUIUI
01.01.2025 10:25Не больше, чем абстракция концепта собаки, с чем умеют работать не только люди.
А вот с отрицательными числами, невычислимыми (в алгоритмическом смысле) вещественными, или уж тем более комплексными так не получится — у них нет прямых реализаций в реальном мире.
kciray Автор
01.01.2025 10:25которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Почему? В книге по теории типов, вполне четко объясняется параллель между теорией типов и реальной математикой, и дается конкретный пример теоремы Безу. И сама теория типов тоже довольно четко выстроена (на уровне метатеории).
Как быть с математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих
Можете взять любой учебник по теории автоматов и ознакомиться. Игра жизни - это клеточный автомат. Отлично она формализуется, как и Машина Тьюринга. Они все довольно четко выражены в теории множеств. Трудность может быть только в том, чтобы конфигурацию машины Тьюринга в конкретный момент времени, и потом задать правило перехода от предыдущей к последующей
kciray Автор
01.01.2025 10:25А никак. Этому не учили.
Обучение и развитие человека намного шире и может выходить за рамки того, что "учили".
Можно же обучаться самостоятельно (по книге или курсу), а также внутри IDE или симулятора. А еще можно проводить исследовательскую работу.
RikkiMongoose
01.01.2025 10:25Ну, можно вообще на ассемблере всё писать. Или даже в шестнадцатеричном коде.
Или можно всю жизнь проводить исследовательскую работу по выпеканию квадратного блина на круглой сковородке.
Zenitchik
01.01.2025 10:25Вы боретесь с ветряными мельницами.
Абстракция над абстракцией нужна для поиска более общих инструментов работы с абстракциями. Всего навсего.
Если у кого-то там сектантский апломб - Вам-то что за беда? Отвечать сектантским апломбом на сектантский апломб - нездоровая манера.
RikkiMongoose
01.01.2025 10:25Собственно, я уже итак довольно глубоко проработал эту область и прошел 2/4 курса из специализации на Курсере по дизайну и анализу алгоритмов от Стендфордского университета в 2022 году. Моя главная цель — это не только комфортное прохождение алгоритмических собесов и сильная позиция на рынке, но еще и возможность брать более крутые и интересные задачи.Если вы закончили университет в 15 году (примерно 10 лет назад), то примерно к 40 годам вы такими темпами станете стажёром в Яндексе. (именно на тамошних собеседованиях, которых станет к тому времени где-то 7-8 подряд, вам и может пригодиться знание дизайна и анализа алгоритмов)
20 лет я учился недаром,
Пыль наук не напрасно глотал.
Есть теперь у меня, чем гордиться -
Мой оклад, как у дворника стал!kciray Автор
01.01.2025 10:25На стажера спрашивают совсем-совсем простые алгоритмы вроде цикла for по массиву.
Ваше сообщение составлено без опыта собеседований и понимания реальной ситуации на рынке, а также без знаний ситуации с алгоритмическими собеседованиями. Например, в некоторые команды Яндекса принимают по сокращенной программе собеседований, в которой только 2 технических (алгоритмических) собеседования. По личному опыту, я проходил в команду Яндекс.Медиасервисы в 2021 году на 17-й грейд (это эквивалент Синьера). И там не было чего-то особо сложного, среднего уровня типовые задачи.
RikkiMongoose
01.01.2025 10:25Расскажите больше о вашем "понимании реальной ситуации на рынке". Где и когда срочно стали требоваться специалисты по Coq и эндофункторам?
redbeardster
01.01.2025 10:25В некоей отечественной финтех-конторе технари аппрувят кандидата после слова "Coq" (умение или готовность его изучить и применить). Если добавить "Rust" (лучше - реальный скилл) - Вы приняты (если не запорете интервью с менеджментом) :)
RikkiMongoose
01.01.2025 10:25Но название этой конторы никто не знает
redbeardster
01.01.2025 10:25Знают, и очень хорошо. Начинается на "Ex... "
piton_nsk
01.01.2025 10:25Видимо знают в неких очень узких кругах.
RikkiMongoose
01.01.2025 10:25Да вот же она: https://career.habr.com/companies/excorp
Там так и написано: "для нас твои 5000+ часов в CS являются конкурентным преимуществом"
kciray Автор
01.01.2025 10:25Интересно, зачем им Coq, они же "EX CORP. Мы создаем экосистему сервисов для игроков соревновательных игр"
kciray Автор
01.01.2025 10:25твои 5000+ часов в CS
Может тут имеется в виду чистое программирование в любом виде или решение алгоритмических задач?
IUIUIUIUIUIUIUI
01.01.2025 10:25В каждом втором блокчейне. IOHK (которые cardano), например, много чего на агде делают. Кое-какие другие блокчейны имеют или разрабатывают формализации на coq/isabelle/etc.
RikkiMongoose
01.01.2025 10:25Как выглядит доказательство правила Де-Моргана (¬(A ∧ B) ⇒ (¬A ∨ ¬B)) на самом низком уровне
Underskyer1
01.01.2025 10:25Прежде всего, спасибо за статью. Тут очень много всего, не мало интересного и есть даже что-то полезное)))
Теория множеств - это больше про классификацию объектов, в частности, про отношение таких классификаций. Из неё пытались соорудить фундамент всея математики, но получилось не очень.
Поэтому попробовали развить теорию типов - у каждого терма есть свой тип, что позволяет проверять корректность алгоритмов, опираясь на утверждения об отношениях типов. И это, конечно здорово, но пришлось расширять теорию вселенными типов, включать в неё и значения... В общем, выяснилось, что "обычных" типов маловато, чтобы свести концы с концами.
Теория категорий - раздел топологи, позволяющий формализовать различные утверждения о путях. Между множествами, классами, типами, значениями и практически всем, что можно вообразить. Для программистов и других физиков прежде всего важны пути вычислений, в частности, задача о нахождении оптимального алгоритма. До сих пор идут исследования о роли множеств в теории категорий... Но ИМХО тема всё равно интересная.
В связи с этим вопрос: зачем вообще пытаться реализовать теорию множеств в теории типов, с её аксиомами выбора и проч.? Например, для тех же действительных чисел куда полезнее понятие типа, чем множества. И вообще зачем заморачиваться с неконструктивной математикой, если априори известно, что это бесполезный математический онанизм?
kciray Автор
01.01.2025 10:25но получилось не очень.
Почему не очень? Вроде неплохо получилось, технически все сходится и выводится. Иногда очень долго и не всегда красиво, но все равно оно работает и адекватной замены аксиоматической теории множеств я пока не вижу. Ну разве что, coq вроде неплохо через индуктивные типы многие штуки представляет.
зачем заморачиваться с неконструктивной математикой, если априори известно, что это бесполезный математический онанизм?
А все классические учебники по анализу\теории вероятности, они же сильно неконструктивные, там каждая третья теорема использует аксиому исключения среднего в явной или неявной форме. Если только конструктивный подход использовать, есть учебник по конструктивной теории множеств и конструктивному анализу, но мне они показались весьма экспериментальными...
Underskyer1
01.01.2025 10:25На сколько помню, появление теории типов было обусловлено тем, что теория множеств приводила к парадоксам, которые не позволяли считать её надёжным фундаментом. Требовался другой язык для целей формализации корректности алгоритмов.
Получается, что неконструктивная математика важна только потому, что на неё опираются старые учебники?)) Выглядит так, что любые неконструктивные теоремы попросту бесполезны, потому что... неконструктивны! Это просто демагогия, когда в фундаменте всех рассуждений лежит аксиома "потому что можем и всё тут!" Проверка каких-либо условий для частных случаев не даёт алгоритмов получения таких результатов, что обесценивает эту проверку.
Прощу прощения за наивность суждений, я дилетант в математике) Но надеюсь, что меня или переубедят, или согласятся со мной (или пошлют в правильном направлении)))
kciray Автор
01.01.2025 10:25появление теории типов было обусловлено тем, что теория множеств приводила к парадоксам
Это было самым-самым началом. Потом теорию множеств пофиксили и сейчас в ZFC нет парадоксов
что обесценивает эту проверку.
Я бы не сказал, что обесценивает. Но тут надо уточнить, что вы имеете в виду под неконструктивной математикой? Вы не признаете аксиому исключения третьего, или шире понимаете неконструктивность?
Underskyer1
01.01.2025 10:25Я понимаю конструктивное доказательство так: это последовательный вывод утверждения по правилам на основании начальных условий и базовых аксиом. Например, доказательством обитаемости типа является только предоставление его экземпляра (корректный алгоритм его вывода, завершающийся за конечное время), а не какое-то иное доказательство того, что тип НЕ необитаем. Аксиома выбора также бесполезна с практической точки зрения - если нет универсального (для любого множества) алгоритма выбора его элемента, то тут и говорить не о чем.
kciray Автор
01.01.2025 10:25А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?
Underskyer1
01.01.2025 10:25"Доказать", и "вывести" (получить алгоритм вывода) - это разные цели. Они совпадают только в случае конструктивного доказательства. Алгоритмы полезны тем, что их можно переиспользовать - они помогают в решении целого класса задач с разными начальными условиями. Неконструктивные доказательства бесполезны. От слова "совсем". Вы можете "доказать всякие штуки из теории чисел", но в этом не будет никакого смысла, если вы при этом опираетесь на аксиому "потому что!" и не получите алгоритмов для решения каких-либо практических задач.
Каждая статически-типизированная компьютерная программа представляет собой доказательство выводимости значения типа-результата, если есть значение (утверждение истинности!) типа-начального-условия. Т.е. корректная с точки зрения синтаксиса языка программа по факту является конструктивным доказательством своей корректности. Доказать такую программу-теорему можно ещё до её исполнения.
А вот иное доказательство того, что тип программы A => B не является пустым типом, но при этом сама реализация (значение типа A => B) не предоставляется - неконструктивно. Это просто бесполезное доказательство.
kciray Автор
01.01.2025 10:25Я пытаюсь найти мотивацию, чтобы полностью отказаться от неконструктивной математики, но пока что не получается...
Zenitchik
01.01.2025 10:25А она Вам чем-то мешает? Мы в жизни делаем много неконструктивного. Чем неконструктивная математика хуже?
kciray Автор
01.01.2025 10:25Мне - комфортно и с неконструктивной. Но комментатор выше написал "любые неконструктивные теоремы попросту бесполезны" и я пытаюсь понять, что имелось в виду
blaze79
01.01.2025 10:25А у меня курс матанализа начинался с теории множеств и CFT (там лемма Цорна страшна), из нее легко выводятся натуральные числа и их аксиомы
piton_nsk
01.01.2025 10:25Глубоко понять, как устроен реальный мир на низком уровне. У меня еще со школы сохранилась мечта — написать программу, которая из законов квантовой физики выводит таблицу Менделеева и предсказывает химические реакции, а также закладывает фундамент химии.
Про таблицу Менделеева вроде еще в школе рассказывают, электронные орбитали, валентные электроны, принцип запрета Паули и вот это вот все.
в ближайшем будущем я могу попробовать освоить и формализовать дифференциальные уравнения
Что значит освоить дифференциальные уравнения?
Развитие в менеджмент. У меня сложилось впечатление, что хорошие менеджеры (особенно топ‑менеджеры) — это весьма образованные люди и они максимально используют математику в работе. Речь идет не только о простом статистическом анализе данных, но еще и о построении и проверке гипотез, использовании инструментов Data Science, а также применении всяких интересных штук типа Теории Игр/Теории оптимизации/Линейного программирования для принятия крупных стратегических решений.
А на основании чего у вас сложилось такое впечатление? Что-то не верится что топ-менеджеры рассказывают вам как они принимают "крупные стратегические решения".
Собственно, можно попробовать развиваться по этому пути и заработать очень много денег
Воротилы бизнеса уже держат мешки с деньгами наготове для математического менеджера.
kciray Автор
01.01.2025 10:25электронные орбитали, валентные электроны, принцип запрета Паули и вот это вот все
Хотелось бы разобраться, откуда это все следует
piton_nsk
01.01.2025 10:25Атомные орбитали заполняются по определенным правилам - принцип Паули, приоритет наименьшей энергии, правило Хунда. Орбитали берутся из уравнения Шредингера. Вот и таблица Менделеева.
kciray Автор
01.01.2025 10:25А на основании чего у вас сложилось такое впечатление?
Личный опыт и общение с такими людьми, а также чтение их статей и истории их жизни\карьеры
Воротилы бизнеса уже держат мешки с деньгами наготове
Ну вообще для DataScience-спецов держат, а это оно и есть
piton_nsk
01.01.2025 10:25Ну вообще для DataScience-спецов держат, а это оно и есть
DataScience и менеджерство вещи сильно разные. Но я бы посмотрел как спец по условному матану станет руководить коллективом хотя бы в сотню людей (нематематиков). Со стороны, конечно. Самому в этом участвовать как-то не хочется)
darkkosinus
01.01.2025 10:25Большое спасибо за статью! Я даже восстановил доступ к Хабру впервые за 10 лет, что бы оставить комментарий.
Получив диплом Математика-Программиста я должен с сожалением признать что не доказал сам ни одной теоремы и ни разу не использовал фундаментальные знания за 15 лет работы FullStack разработчиком.
Хотя я помню свое потрясение на семинаре по уравнениям мат. физики (удивительно, но там стоит "хорошо") когда понял что каждая точка реальности может быть формально определенна во всех смыслах.
Но при этом вынужден увидеть себя скорее в категории "менеджеров которые не очень сильны в алгоритмах" и больше получают удовольствия от использования софт скилов и настройки процессов команды для работы с клиентами, и построения грамотной архитектуры при существующих ресурсах.
При этом я отношу себя к тем самым фанатикам которые будут ночью кодить пет-проект на LLM с агентами, потому что это круто, интересно и вообще.
Но опустим)
Если позволите добавить еще одно возможное применение, тк хотелось бы услышать ваше мнение на этот счет.Мне кажется что сейчас все еще очень слаба программная база для работы с квантовыми компьютерами.
И если бы получилось создать систему, которая при заданных параметрах компьютера (кол-во кубитов, методы работы с ошибками, и тд.) и заданных критериях инференса (время работы) смогла бы доказательно найти оптимальную архитектуру ML модели (для решения заданной задачи (например MNIST), то это могло бы действительно фундаментально изменить всю область ИИ.
Zenitchik
А я в меру своего скромного ума, понял, что теория категорий - это следующий уровень абстракции над теорией множеств.
kciray Автор
Как думаете, есть ли смысл в ней разобраться (как она в coq формализуется) и через нее работать? Т.е. выводить теорию множеств из теории категорий, а теорию категорий из теории типов?
Я еще видел учебник "An Invitation to Applied Category Theory. Seven Sketches in Compositionality", вроде неплохое введение
Zenitchik
Не знаю. Я - не разобрался. Как уже сказал, в силу своего скромного ума, я так понял, что она нужна математикам для выведения теорем, которые потом используются в теории множеств и иже с ней. А для прямого практического применения - не уверен.
Я, конечно, математику люблю, но я - не профессиональный математик, и тратить много времени на настолько высокие абстракции - не готов.
IUIUIUIUIUIUIUI
Не очень применимый к чистой математике вопрос. Лучше спрашивать «весело ли это» и «что получится».
В прикладных задачах ничего особо интересного не получится. Весело ли это? Кому как.
Сделано в ETCS. Полезна тем, что можно обобщать над аксиоматикой теории множеств.
Я бы не стал, получится неудобная и неизящная конструкция.
Да, у нас есть системы типов, и есть классы категорий, реализующие внутреннюю логику этих систем типов, но формулировать эти вещи лучше по отдельности и строить соответствие пропозиционально, а не дефиниционально, так сказать.
kciray Автор
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Про ETCS интересно, спасибо.
А как мы ее тогда в теорем-прувере формализовать будем?
IUIUIUIUIUIUIUI
Если вкратце, то потому что чистые математики редко этим руководствуются, и польза вне самой чистой математики оказывается скорее случайным побочным эффектом, чем результатом целенаправленной работы.
Как обычно и как любую другую теорию, просто используя прувер как метаязык.