O зависимых типах и интуиционизме в программировании математики

Обсуждается практическая возможность доказуемого программирования математики на основе подхода конструктивизма и применения языка с зависимыми типами (dependent types, proof carrying code). Принципы конструктивизма и доказуемого программирования объясняются на примерах. Рассмотрение опирается на опыт реализации на языке Agda небольшой библиотеки вычислительной алгебры, включающей арифметику области остатков $R/(b)$ для евклидова кольца $R$.