Beyond Booleans - “bool expressions” in Lean, proposition, proof
(overreacted.io)
from Kissaki@programming.dev to programming@programming.dev on 17 Aug 08:01
https://programming.dev/post/35834039
from Kissaki@programming.dev to programming@programming.dev on 17 Aug 08:01
https://programming.dev/post/35834039
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.
threaded - newest
This is an unbelievably good explanation of some very difficult concepts. I think the Lean documentation should start with an enormous link to this post.
Highly recommended to anyone interested in Lean who isn’t already an expert.