On dependent types and intuitionism in programming mathematics

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)