33
Beyond Booleans - “bool expressions” in Lean, proposition, proof (overreacted.io)
submitted 1 year ago by to c/programming@programming.dev
1 comment fedilink hide all child comments
 

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.

you are viewing a single comment's thread
view the rest of the comments
[–] 8 points 1 year ago

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.

  • permalink
  • fedilink
  • source
    •