Beyond Booleans - “bool expressions” in Lean, proposition, proof

Explores how the Lean programming language handles 2 + 2 = 4, which other programming languages collapse into a bool, but Lean considers a Proposition, and requires Proof.

How does provably correct programming look? This article seems to give a good introduction and example.