Introduction to Formal Verification with Lean Part 1
hashcloak.com
Introduction to Formal Verification with Lean Part 1
1–10 of 55 posts
Re: Introduction to Formal Verification with Lean Part 1
#2[flagged]
Re: Introduction to Formal Verification with Lean Part 1
#3Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).
Small feedback: - Great flow, explaination, motivation and so on! :) - Typo: "conext" at the bottom - If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)
Re: Introduction to Formal Verification with Lean Part 1
#4Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/
Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/
And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/
Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4
This is the best intro to Lean I know, plus it teaches you why a + b = b + a.
Re: Introduction to Formal Verification with Lean Part 1
#5(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
Re: Introduction to Formal Verification with Lean Part 1
#6https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... I like this author and a while ago found that he'd published a book on Lean!
In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.
Re: Introduction to Formal Verification with Lean Part 1
#7(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Re: Introduction to Formal Verification with Lean Part 1
#8(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs, even infinity of them, rather than for the ones that exist in your test.
Re: Introduction to Formal Verification with Lean Part 1
#9(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
I’m an noob to Lean myself, but my best explanation is that asserts are checks that happen at runtime. Imagine compile-time asserts, where the compiler is able to determine the validity of assertions without needing to run the program. Formal verification techniques make this possible. In Lean, it is possible to write a proof that, if true, guarantees that the code works.
Re: Introduction to Formal Verification with Lean Part 1
#10Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot). Small feedback: - Great flow, explai…
Vitalik recently wrote about vibe-coding in Lean and assembly language, using proof verification in Lean, saying "if done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before."