Изоморфизм Карри-Ховарда: Код программы как математическое доказательство
Завершая наш цикл по дискретной математике, мы подходим к глубочайшей философской истине, объединяющей миры софта и чистой логики. Обычно программисты относятся к написанию кода как к ремесленной задаче: заставить компьютер выполнить команды. Математики же доказывают вечные истины. В середине XX века Хаскелл Карри и Уильям Ховард обнаружили, что эти два процесса — абсолютно одно и то же. Это открытие известно как Изоморфизм Карри-Ховарда.