5 ms·

Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works: def main := for

Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works: def main := for i in [1:101] do if i % 15 == 0 then IO.println "FizzBuzz" else if i % 3 == 0 then IO.println "Fizz" else if i % 5 == 0 then IO.println "Buzz" else IO.println s!"{i}" You can run it with `lean --run FizzBuzz.lean`, and you can read more about programming in Lean 4 at https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/.

kristopolous 3y ago
Thanks. I appreciate it. According to $ find leanprover.github.io/functional_programming_in_lean -name \*.html -exec html2text {} \; | wc -w 271248 That's about 1,000 pages. Some of us who are less ambitious and motivated need an under 5-minutes example to feel compelled to engage with such a large amount of documentation. Essentially the problem is "There's hundreds of programming languages I'll never have the time to learn. Show me why I should care about this one and do it quickly." Given that, I actually appreciate the fancy example. It really shows off some interesting features in reaching a goal that's really simple to understand. It looks similar to Haskell in that it approaches programming in a mathematically formal and rigorous way. If you're deeply involved in the project, an example that would be really exciting to me would be a lean version of one of these proofs: https://en.wikipedia.org/wiki/Category:Computer-assisted_proofs https://en.wikipedia.org/wiki/Category:Computer-assisted_pro... or https://en.wikipedia.org/wiki/Computer-assisted_proof#Theorems_proved_with_the_help_of_computer_programs https://en.wikipedia.org/wiki/Computer-assisted_proof#Theore... Start the example with how the proof was initially tackled on a computer and show the challenges faced and then demonstrate how lean can do it more elegantly. I appreciate your time.
- ykonstant 3y ago
  I do not see how you are getting 1000 pages; the pdf is about 400 pages with copious amounts of sparse code blocks, and the introductory stuff (The chapters Getting to know Lean and Hello World) run about 86 pages. Certainly not "Lean in 5 minutes" for sure, but not a spellbook either. In any case, Lean is a proof formalization and verification language doubling as a general purpose programming language still in its research phase. If you are interested in how this sounds, you can check it out. If not, there is no need.
  - kristopolous 3y ago
    I just did a recursive scrape of the tutorial site, converted the html to text, then did a word count using wc and simply divided it by the average number of words per page. Word in this case includes things like '(' and syntax characters. Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial. The point is as an answer to the basic question "what is this and why should I care?" Responding with something over 10 pages is likely unadvisable, yet alone over 100. "Over 100" here is effectively equivalent to "over 5,000". The target should be like 0.25-5, and closer to the 0.25. Elevator pitch it. 1. For (target customers) 2. Who are dissatisfied with (the current market alternative) 3. Lean is a (new product category) 4. That provides (key problem-solving capability). 5. Unlike (the product alternative), 6. Lean (describe the key product features). https://www.elevatorpitchessentials.com/essays/CrossingTheChasmElevatorPitchTemplate.html https://www.elevatorpitchessentials.com/essays/CrossingTheCh...
    - uxp8u61q 3y ago
      If you have to listen to such an elevator pitch, you're not the target audience. This is bleeding-edge math/CS research. Talking about a "product" just shows that you have a fundamental misconception regarding what this is all about.
      - kristopolous 3y ago
        It's a way to describe things. You can describe, for example, the James Webb space telescope or the Large Hadron Collider in that way. You can also describe say, the Frankfurt school of critical theory or every other programming language. A product is an act of production here, as in some kind of process. Even things like classes of clouds and rocks can be described in that framework I don't expect Lean to be an exception Also to respond to the idea that I'm fundamentally unworthy of an explanation: I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. They don't demand advanced physics degrees to unveil its purpose like they're some kind of secret society.
- mauricioc 3y ago
  None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using Lean" section of https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html lists some theorems whose proofs have been verified in Lean, but (despite being written in Isabelle) I think the Kepler Conjecture formalization is the best example of what you have in mind. The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.
incrudible 3y ago
Neither of these examples answer my question: What's the point? Perhaps FizzBuzz is a terrible example for such a language, but I don't see anything being "proved" here. Can it do something like static asserts on the output, without actually running the program? E.g. can you prove that the outputs will never be anything else than "Fizz", "Buzz" or "FizzBuzz"?
- ykonstant 3y ago
  The examples were not meant to answer your question, but the question kristopolous set. Ask your question at top level and some of us, perhaps myself, will answer.
- alimw 3y ago
  Sure! def f (n : Nat) : String := String.append (if n % 3 = 0 then "Fizz" else "") (if n % 5 = 0 then "Buzz" else "") #eval List.map f (List.range 100) theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by unfold f split <;> split · exact Or.inl rfl · exact Or.inr (Or.inl rfl) · exact Or.inr (Or.inr (Or.inl rfl)) · exact Or.inr (Or.inr (Or.inr rfl))
  - alimw 3y ago
    Oops! I checked the spec and it's supposed do something more like this: def f (n : Nat) : String := Option.getD (Option.merge String.append (if n % 3 = 0 then "Fizz" else none) (if n % 5 = 0 then "Buzz" else none)) (toString n) #eval List.map (fun k => f (k + 1)) (List.range 100) theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by unfold f split <;> split · exact Or.inl rfl · exact Or.inr (Or.inl rfl) · exact Or.inr (Or.inr (Or.inl rfl)) · exact Or.inr (Or.inr (Or.inr rfl))
  - harveywi 3y ago
    Awesome! Where did the "split_ifs" tactic come from though? Mathlib? In your opinion does it make sense to do program verification without using Mathlib, or would you recommend just using it pretty much all the time?

kristopolous 3y ago

Thanks. I appreciate it. According to $ find leanprover.github.io/functional_programming_in_lean -name \*.html -exec html2text {} \; | wc -w 271248 That's about 1,000 pages. Some of us who are less ambitious and motivated need an under 5-minutes example to feel compelled to engage with such a large amount of documentation. Essentially the problem is "There's hundreds of programming languages I'll never have the time to learn. Show me why I should care about this one and do it quickly." Given that, I actually appreciate the fancy example. It really shows off some interesting features in reaching a goal that's really simple to understand. It looks similar to Haskell in that it approaches programming in a mathematically formal and rigorous way. If you're deeply involved in the project, an example that would be really exciting to me would be a lean version of one of these proofs: https://en.wikipedia.org/wiki/Category:Computer-assisted_proofs https://en.wikipedia.org/wiki/Category:Computer-assisted_pro... or https://en.wikipedia.org/wiki/Computer-assisted_proof#Theorems_proved_with_the_help_of_computer_programs https://en.wikipedia.org/wiki/Computer-assisted_proof#Theore... Start the example with how the proof was initially tackled on a computer and show the challenges faced and then demonstrate how lean can do it more elegantly. I appreciate your time.

ykonstant 3y ago
I do not see how you are getting 1000 pages; the pdf is about 400 pages with copious amounts of sparse code blocks, and the introductory stuff (The chapters Getting to know Lean and Hello World) run about 86 pages. Certainly not "Lean in 5 minutes" for sure, but not a spellbook either. In any case, Lean is a proof formalization and verification language doubling as a general purpose programming language still in its research phase. If you are interested in how this sounds, you can check it out. If not, there is no need.
- kristopolous 3y ago
  I just did a recursive scrape of the tutorial site, converted the html to text, then did a word count using wc and simply divided it by the average number of words per page. Word in this case includes things like '(' and syntax characters. Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial. The point is as an answer to the basic question "what is this and why should I care?" Responding with something over 10 pages is likely unadvisable, yet alone over 100. "Over 100" here is effectively equivalent to "over 5,000". The target should be like 0.25-5, and closer to the 0.25. Elevator pitch it. 1. For (target customers) 2. Who are dissatisfied with (the current market alternative) 3. Lean is a (new product category) 4. That provides (key problem-solving capability). 5. Unlike (the product alternative), 6. Lean (describe the key product features). https://www.elevatorpitchessentials.com/essays/CrossingTheChasmElevatorPitchTemplate.html https://www.elevatorpitchessentials.com/essays/CrossingTheCh...
  - uxp8u61q 3y ago
    If you have to listen to such an elevator pitch, you're not the target audience. This is bleeding-edge math/CS research. Talking about a "product" just shows that you have a fundamental misconception regarding what this is all about.
    - kristopolous 3y ago
      It's a way to describe things. You can describe, for example, the James Webb space telescope or the Large Hadron Collider in that way. You can also describe say, the Frankfurt school of critical theory or every other programming language. A product is an act of production here, as in some kind of process. Even things like classes of clouds and rocks can be described in that framework I don't expect Lean to be an exception Also to respond to the idea that I'm fundamentally unworthy of an explanation: I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. They don't demand advanced physics degrees to unveil its purpose like they're some kind of secret society.
mauricioc 3y ago
None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using Lean" section of https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html lists some theorems whose proofs have been verified in Lean, but (despite being written in Isabelle) I think the Kepler Conjecture formalization is the best example of what you have in mind. The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.

incrudible 3y ago

Neither of these examples answer my question: What's the point? Perhaps FizzBuzz is a terrible example for such a language, but I don't see anything being "proved" here. Can it do something like static asserts on the output, without actually running the program? E.g. can you prove that the outputs will never be anything else than "Fizz", "Buzz" or "FizzBuzz"?

ykonstant 3y ago
The examples were not meant to answer your question, but the question kristopolous set. Ask your question at top level and some of us, perhaps myself, will answer.
alimw 3y ago
Sure! def f (n : Nat) : String := String.append (if n % 3 = 0 then "Fizz" else "") (if n % 5 = 0 then "Buzz" else "") #eval List.map f (List.range 100) theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by unfold f split <;> split · exact Or.inl rfl · exact Or.inr (Or.inl rfl) · exact Or.inr (Or.inr (Or.inl rfl)) · exact Or.inr (Or.inr (Or.inr rfl))
- alimw 3y ago
  Oops! I checked the spec and it's supposed do something more like this: def f (n : Nat) : String := Option.getD (Option.merge String.append (if n % 3 = 0 then "Fizz" else none) (if n % 5 = 0 then "Buzz" else none)) (toString n) #eval List.map (fun k => f (k + 1)) (List.range 100) theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by unfold f split <;> split · exact Or.inl rfl · exact Or.inr (Or.inl rfl) · exact Or.inr (Or.inr (Or.inl rfl)) · exact Or.inr (Or.inr (Or.inr rfl))
- harveywi 3y ago
  Awesome! Where did the "split_ifs" tactic come from though? Mathlib? In your opinion does it make sense to do program verification without using Mathlib, or would you recommend just using it pretty much all the time?