Abstract:
It is discussed a practical possibility of a provable programming of mathematics basing of the approach of intuitionism, a language with dependent types, proof carrying code. This approach is illustrated with examples. The discourse bases on the experience of implementing in the Agda language of a certain small algebraic library including the arithmetic of a residue domain $R/(b)$ for an arbitrary Euclidean ring $R$. (in Russian)
Key words and phrases:intuitionistic mathematics, algebra, dependent types, Coq, Agda, Haskell.