Constructing provable programs for arithmetic of natural numbers in binary representation

Support for dependent types in a functional programming language Agda makes it possible to include machine-checked proofs in the program. The problem of provable inclusion of algorithms for arithmetic operations on natural numbers in binary representation is considered.
A library of evidentiary programs for “written calculation” algorithms, acting on bit lists has been built. It contains machine-verifiable proofs of the required properties of the applied algorithms, corrects and substantially supplements the Bin part of the lib-0.16 standard library of the Agda language. (In Russian).