Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Introduction to Formal Verification with Lean Part 1

hashcloak.com

Post reply on HN
Print view View original

41–50 of 55 posts

Re: Introduction to Formal Verification with Lean Part 1

#41

Post by siknad »

EGreg wrote: post #28

Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs? I found that out when reading the recent articls about counterexamples.

Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).

Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.

Re: Introduction to Formal Verification with Lean Part 1

#42

Post by 8note »

This is cool and im not familiar with what lean actually does beyond the words "formal methods"

immediate questions from reading:

* what is rfl?

* what is decide?

i spent a lot of time looking for where these keywords(? declarations?) were made and i still dont know what they end up meaning

Re: Introduction to Formal Verification with Lean Part 1

#43

Post by nylonstrung »

kccqzy wrote: post #21

I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…

The @[grind] tactic has to be the single most important addition to Lean in terms of it's growing popularity

Re: Introduction to Formal Verification with Lean Part 1

#44

Post by derdi »

Gajurgensen wrote: post #24
kccqzy wrote: post #21

I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…

I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn…

Very well put. I'll just add that there is one more thing one can do to document the important/insightful/interesting parts of a proof, where it makes sense: Write a comment.

Re: Introduction to Formal Verification with Lean Part 1

#45

Post by derdi »

8note wrote: post #42

This is cool and im not familiar with what lean actually does beyond the words "formal methods" immediate questions from reading: * what is rfl? * what is decide? i spent a lot of time looking for where these keywords(? declarations?) were made and i still dont know what they end up meaning

These are both "tactics". The article defines tactics as "instructions that help reduce the current goal". Writing a proof consists of starting with the thing to be proved and then writing a sequence of tactics to break the problem up into progressively easier and easier problems, until everything is broken down into things that are trivially true.

"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.

"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.

Re: Introduction to Formal Verification with Lean Part 1

#46

Post by badcryptobitch »

georgespencer wrote: post #35
botencat wrote: post #34

Please please please don't hijack scrolling :(

…and for no discernible reason, too. Ordinarily, irritating stuttering pages like this at least do some sort of visually fun thing. This is just a diabolical Framer design with a ton of needlessly overlapping nested containers. I deleted more than 20 invisible divs from the DOM and scrolling improved dramatically. I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI s…

I'm the webmaster. Another commenter let me know about the scrolling. I'll get onto it. Thank you for the feedback

Re: Introduction to Formal Verification with Lean Part 1

#47

Post by rramadass »

rik-x wrote: post #5

(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?

Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively.

Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"

Some simple tutorials;

Introduction to Lean for Programmers: The syntax and semantics of mathematics - https://towardsdatascience.com/introduction-to-lean-for-prog...

The hitchhiker's guide to reading Lean 4 theorems - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...

Re: Introduction to Formal Verification with Lean Part 1

#48

Post by [deleted] »

kccqzy wrote: post #21

I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…

[deleted]

Re: Introduction to Formal Verification with Lean Part 1

#49

Post by black_knight »

Gajurgensen wrote: post #24
kccqzy wrote: post #21

I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…

I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn…

I feel like there is a lot of interesting things one can do in proof engineering without resorting to "tactics" (meta-programs searching for the proof). In some cases one can replace them by robust lemmas which show general results. Or the language could have good support for abstractions (dependent types already give us a lot of power here!).

Personally, I am experimenting a lot with Agda's instance arguments these days. They somehow have a bad rep for being slow, but their performance has improved a lot! One can juice it to write really readable code (Like truly ad-hoc polymorphic operators, or declaring axioms used in a theorem like `⦃ AC ⦄ → Theorem`), but it also allows for proof searches. Contrary to “tactics”, instance arguments feel like a fluid part of the proof language.

I think there is a lot of room for innovation in the space of proof engineering. I really hope that LLMs will not suck all the oxygen out of the room, by being trained on existing dogmas.

Re: Introduction to Formal Verification with Lean Part 1

#50

Post by badcryptobitch »

badcryptobitch wrote: post #46
georgespencer wrote: post #35

Earlier quoted context omitted.

…and for no discernible reason, too. Ordinarily, irritating stuttering pages like this at least do some sort of visually fun thing. This is just a diabolical Framer design with a ton of needlessly overlapping nested containers. I deleted more than 20 invisible divs from the DOM and scrolling improved dramatically. I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI s…

I'm the webmaster. Another commenter let me know about the scrolling. I'll get onto it. Thank you for the feedback

I've fixed it. Again, thank you for the feedback
Post reply on HN