Программирование основ вычислительной алгебры на языке с зависимыми типами

В статье описываются главные черты разработанной автором на основе доказательного программирования библиотеки вычислительной алгебры. Обсуждается опыт доказательного программирования некоторых классических категорий вычислительной алгебры («группа», «кольцо» и так далее) на основе подхода конструктивизма, применения языка с зависимыми типами, построения машинно-проверяемых доказательств (dependent types, proof carrying code). Выявляются проблемы, связанные с этим подходом, и отмечаются дополнительные возможности, даваемые применением аппарата зависимых типов. В качестве инструмента используется функциональный язык Agda. Статья является продолжением вводной статьи автора в данном журнале за 2014 год.