Как вывести квин из теоремы Клини о рекурсии — и заодно построить его в лямбда-исчислении
Constructing a Quine from Kleene's Second Recursion Theorem
Автор разбирает, как из второй теоремы Клини о рекурсии получается квин — программа, печатающая собственный исходник. Сначала теорема формулируется классически через нумерацию частично рекурсивных функций, затем в функциональном стиле с квази-квотером, а попутно всплывают диагональная лемма, теоремы Гёделя и Тарского. Всё это доводится до рабочего квина в нетипизированном лямбда-исчислении с кодированием Чёрча, проверенного в Rocq.
Формализация — вовсе не механическая рутина: сам процесс может быть источником озарений и творчества; кстати, именно поэтому я считаю, что популярный взгляд на формальную верификацию как на простое переписывание упускает суть.