RetroFed Forum
Your home away from modern life.
Beyond Booleans - “bool expressions” in Lean, proposition, proof
Post Reply
AuthorMessage
Kissaki programming.dev Kissaki@programming.dev
Joined: 2023-06-11
Quote

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.

1   Original
Post Reply
Back to top