This book applies a deductive approach to programming based on combining programs with abstract mathematical theories that ensure their work. The descriptions of these theories, the algorithms recorded in terms of these theories, and the theorems and lemmas describing their properties are presented together. The implementation of algorithms in a real programming language is the central theme of the book. This book is intended for those who seek a deeper understanding of the essence of programming, whether professional programmers or scientists and engineers, for whom programming is an important part of their professional activities. The book is intended to be read from beginning to end. Readers will only be able to understand the material by studying the code, proving the lemmas, and doing the exercises.