Programming basic computer algebra in a language with dependent types

The article describes the main features of the computational algebra library developed by the author on the basis of proving programming. The experience of demonstrative programming of some classical categories of computational algebra ("group", "ring" and so on) is discussed on the basis of the constructivist approach, the use of language with dependent types, the construction of machine-verified proofs (dependent types, proof carrying code). The problems associated with this approach are identified, and additional possibilities are indicated, given by the use of a device of dependent types. The instrument is the functional language Agda. The article is a continuation of the introductory article of the author in this magazine for 2014