Как понять в программировании всё

Типовая схема обучения программированию, причём на всех уровнях фактически, с нуля до сеньора, и во всех форматах, от учебников и видеолекций до курсов и университетов, что движемся от простого к сложному. И я по этой схеме тоже учу, пока ещё :)

Вроде бы это правильно: научился сперва кодить скрипт на 10-100 строк, потом на тысячу, потом на 3-5-10 тысяч, попутно изучаешь конкретный стек технологий, и потом этим стеком пытаешься вписаться куда-то на работу. Ну а дальше по жизни, куда кривая вывезет.

И получается, что вся по сути профессиональная карьера ставится в полную зависимость от случая, от конкретной работы, от конкретного окружения, где тебя постоянно принуждают к ограниченным технологиям. Может и повезёт, если организация поддерживает развитие сотрудников, но это тоже редкость -- боссы традиционно боятся, что как выучится человек прогрессивному, так сразу и уйдёт. Возможность самообучаться в свободное время, когда уже работаешь, резко падает, энергии мало, ну какой-то минимум изредка изучать, чтобы не очень отставать (от непонятно чего), и так всю жизнь. Не будет желания развиваться уже, продакшен всё скушает.

Но есть и другой путь, своеобразный хак -- сперва, потратив конечно время, несколько тысяч часов, двинуть в самый программистский топ, на вершину эволюции разработчика :) И вот уже оттуда, орлиным взглядом можно спокойно обозревать весь айтишный пейзаж, понимая абсолютно всё, абсолютно любой программистский материал, абсолютно любые системы, архитектуры, концепции, языки. И понимая также, как можно сделать это всё гораздо круче.

Короче говоря, эта вершина -- полиморфное лямбда-исчисление высшего порядка с зависимыми типами, высший узел, так сказать, в лямбда-кубе Барендрехта. Это языки Agda, Idris, Coq, F*. Есть ещё альтернатива -- System F (ML-языки, Haskell), но послабее в плане потенциала.

Как добраться на эту вершину разумными усилиями, дальше рассмотрим. Пока главный вопрос -- какая же связь этого куба с профессиональной карьерой?

10 лет назад Владимир Воеводский изменил весь мир, организовав проект унивалентных оснований математики -- это в частности, способы создания формальных языков, ориентированных на вычислительные модели обычных компьютеров, и с помощью таких языков можно автоматизировать математические доказательства (проверять их).

В более прикладном формате эта работа получила название Гомотопическая теория типов (HoTT), которая базируется на теории типов Мартина-Лёфа (MLTT).

Сегодня языки из вершины лямбда-куба применяются например для верификации исходных текстов программ, для создания очень надёжного софта. Безусловно, именно из этой концепции вырастет и технологическая сигнулярность -- программы которые пишут программы которые пишут програмы (automatic programs synthesis).

И, что особенно важно, и в этом ключевая идея данного хака, MLTT/HoTT позволяет создавать оригинальные "доверенные" языки программирования, правильность которых исходно доказана математически. Условно говоря, тайп-чекинг не пропустит никакой потенциально опасный код. Пишете систему для банка, и уже на уровне системы типов потенциально исключаются любые некорректные переводы денег например.

При этом вы работаете на очень высоком уровне абстракции. Вы формируете в мозгу уникальный навык моделирования, который в принципе нельзя сформировать программированием на обычных языках, или даже на Хаскеле.

Вы будете прозрачно видеть, как конструировать любую, сколь угодно сложную систему с правильными свойствами, как доказывать её корректность математически. Вы описываете на завтипчиках формальную модель, а потом можете просто заэкстрактить её в Java, или транслировать в Python (из нетипизированной лямбды конечно).

То есть, вы получаете мощнейший инструмент -- умение создавать, условно говоря, MLTT-языки, и вот на этом умении сможете въезжать в совершенно любую сферу разработки. Например, сейчас Machine Learning активно развивается -- но по-хорошему, надо лет пять чтобы погрузиться в тему как следует, и конкуренты тоже активно учатся и движутся вместе с вами по одной и той же массовой широкой магистрали, а за это время само ML далеко убежит. Вы же сможете предлагать уникальный сервис, где вообще нету конкурентов -- разработку мощных языков программирования (верифицированных!) под конкретные ниши ML, с доказательством корректности кода. Или другой вариант -- Microsoft недавно выпустила язык Q# для квантовых вычислений, и вот выложить на гитхаб MLTT-системку для него, совершенно реальный шанс схантиться в Редмонт. Совсем прозаическое -- что-то хотя бы на уровне System F для 1C :)

Причём вот это вот всё стало доступным для всех буквально в последние лет пять. До этого и инструменты, и сами языки были далековаты от продакшена -- и именно сегодня пришло их время.

Ну и в любом случае, вы научитесь мыслить в программировании так, как никто больше практически, ну может несколько сотен человек во всём мире. Это объективно самый программистский топ.

Вы встанете вровень с Джеймсом Гослингом и Ван Россумом, Аланом Кеем и Андерсом Хейлсбергом, Юкихиро Мацумото и Грейдоном Хоаром. Это проект саморазвития даже не на одну жизнь, а на многие жизни вперёд. Вы тогда будете не снизу вверх смотреть на любые программистские темки, постоянно утыкаться в бесконечные стеки-языки без глубокого понимания, тратить кучу времени на их изучение, а сверху вниз -- вообще молниеносно въезжать.

Придумал это всё не я конечно, это такая выжимка опыта небольшой тусовки мега-программистов, которые очень успешно этот путь прошли, а мы двинемся следом, дальше буду приводить ссылки на таких гуру.

Но, на вершину лямбда-куба ведёт весьма узкая тропинка. Материалов много, они несистематизированы, на русском вообще почти нету ничего, и вот главное тут, как существенно ускорить этот подъём.

Схема такая:

— разумно минимизировать изучение математики

- пошаговый алгоритм изучения на практике только самого необходимого

- быстро получать конкретные результаты

Цель: начиная с уровня моего первого курса по алгоритмам, уже через полгода выложить на гитхаб свой MLTT-язык, например для AI/ML под PyTorch.

продолжение следует

Источник: m.vk.com

Комментарии: