Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • This Lean stuff is gibberish and I don't understand why somebody thinks it's going to somehow make things better or simpler to understand.
    by watt
  • I’m curious whether people can use Lean primarily as a software specification language, without necessarily intending to prove everything.

    Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.

    by woggy
  • Please do not try to understand Lean or proof assistants without first getting a rudimentary understanding of the logic involved. This article sort of skips over it, which is reasonable because it is pretty involved.

    Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.

    Here is some necessary reading, feel free to find better sources but wikipedia is good too.

    * Proof trees - https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

    * Constructive/Intuitionistic logic - https://en.wikipedia.org/wiki/Intuitionistic_logic

    * Proofs and Types - https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

    * (In)completeness - https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

    * Compactness - https://en.wikipedia.org/wiki/Compactness_theorem

    by fooker
  • the interface between specification and proof is not so clear, as one often has to look at the proof to understand the spec. And if we see something weird in the proof, that’s a good indication that something is off.

    Yeah this is like if I say something is green how do you know that my green is your green? The proof of the mathematically modeled system is in no shape attached to the symbols that implement it unless its the same program or youre doing trace refinement. And then theres no way of proving that the program is correct in serving the business function unless you run it out. Quite computationally irreducible, the state machine of building state machines

    by whattheheckheck
  • OP: Your article shows “[Contents]” where presumably the table of contents is to be displayed.
    by WalterGR
  • If you don't use a formal tool like Lean to define your spec, then your C++, Rust, or other implementation effectively becomes the spec.

    So “you might get the spec wrong” applies either way. The big difference is that with Lean, you can prove that the implementation matches the spec. With mainstream programming languages, you can't.

    by deterministic
  • So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
    by thom

Explore Birbla archives