Beyond Booleans — overreacted
overreacted.io
What is the type of 2 + 2 = 4?

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.

  • FizzyOrange@programming.dev
    8·
    2 days 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.