Rado Kirov shows that formalization transforms how mathematicians think about structure and collaboration. My work begins from the same premise, but in the world of programming and system software. I aim to bring formal structure to programming itself, treating algorithms, operating systems, and programming languages as subjects that can be expressed with the same rigor as mathematics.
Elements of Programming presents programming as a mathematical discipline built on structure, logic, and proof. Written in the style of Euclid’s Elements, it defines computation through clear axioms, postulates, and propositions. Each book develops one aspect of programming as a coherent system of reasoning.
Book I establishes identity, transformation, and composition as the foundations of computation.
Book II introduces algebraic structures such as categories, functors, and monads.
Book III unites operational and denotational semantics to show that correctness means equivalence of meaning.
Book IV formalizes capability-based security and verification through invariants and confinement.
Book V connects type theory with formal assurance, explaining how types embody proofs.
Book VI extends these ideas into philosophy and ethics, arguing that software expresses human intention and responsibility.
I just released my treatise yesterday, at https://leanpub.com/elementsofprogramming
Elements of Programming presents programming as a mathematical discipline built on structure, logic, and proof. Written in the style of Euclid’s Elements, it defines computation through clear axioms, postulates, and propositions. Each book develops one aspect of programming as a coherent system of reasoning.
Book I establishes identity, transformation, and composition as the foundations of computation.
Book II introduces algebraic structures such as categories, functors, and monads.
Book III unites operational and denotational semantics to show that correctness means equivalence of meaning.
Book IV formalizes capability-based security and verification through invariants and confinement.
Book V connects type theory with formal assurance, explaining how types embody proofs.
Book VI extends these ideas into philosophy and ethics, arguing that software expresses human intention and responsibility.