Formal proofs have been fashionable in the recent months, after being at best an afterthought of the programming community for half a century. By formal proofs I mean writing mathematical statements and their proofs in a computer readable language such that a program (often called a proof assistant) can check that the proof indeed proves the theorem.
Formal proofs belo...