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