Без названия

lex_kravetski — 23.08.2025 С трудом дочитав совершенно идиотскую книгу про Lean, начал читать вторую. Выбор, если что, из двух книг. Язык почему-то не особо известен широким массам и дофига книг про него не написали. Интересно, почему же?

Процитирую пару абзацев из второй главы (первая была про общие слова о пользе Lean в народном хозяйстве).

«Именно этот подход используется в исчислении конструкций, а следовательно, и в Lean. Тот факт, что правила импликации в системе доказательств для естественной дедукции точно соответствуют правилам, управляющим абстракцией и применением функций, является примером изоморфизма Карри-Ховарда, иногда называемого парадигмой предложений как типов. Фактически, тип Prop является синтаксическим сахаром для Sort 0, самого низа иерархии типов, описанной в предыдущей главе. Более того, тип u также является просто синтаксическим сахаром для Sort (u+1). Prop обладает некоторыми особенностями, но, как и другие универсумы типов, он замкнут относительно конструктора стрелок: если у нас есть p q : Prop, то p → q : Prop.

Существует как минимум два способа представления предложений как типов. Для тех, кто придерживается конструктивного взгляда на логику и математику, это верное представление того, что значит быть предложением: предложение p представляет собой своего рода тип данных, а именно, спецификацию типа данных, составляющих доказательство. Доказательство p в таком случае — это просто объект t : p соответствующего типа.»

Стоит ли говорить, что из всех использованных тут сложно звучащих терминов, ранее фигурировали только Sort и Prop. Всё остальное упомянуто впервые. Вот так мы узнаем, что, сцуко, человек, который не умеет программировать на Lean и использовать его для доказательств, сначала должен узнать про изоморфизмы Карри-Ховарда, про конструктивистскую логику, парадигму предложений как типов, конструкторы стрелок и дохера чего ещё, что упоминается в соседних абзацах. Но скорее всего он про это не знает, поэтому ему остаётся только восхититься умом и широчайшими познаниями авторов книги, а также их неспособностью объяснить хоть что-то хоть кому-то. Подозреваю, некоторые фрагменты своей книги они сами через год после её написания уже не смогут понять.

Обе книги в светлом будущем следует рассматривать как наглядные пособия по теме: «Как придумать без балды хорошую штуку, а потом всрать её целиком на этапе популяризации».

Оставить комментарий

Популярные посты:

• Ранее
• Архив