6 ms·
My first verified imperative program
- SUPERX_112 1y agonice
- revskill 1y agoU must have at least 5 characters to get an upvote.
- deleted 1y ago[deleted]
- deleted 1y ago[deleted]
- deleted 1y ago[deleted]
- Joker_vD 1y agoNaturally, this proof only works for arbitrary-precision integers: when you use fixed-precision integers, the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1] or (if you insist on C semantics) [UINT_MAX, 1]. Hopefully the proof would break if one tried to transfer it over?
- Jtsummers 1y ago> the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1] `INT_MIN + -1` is not 0 so it should report false in that case. For UINT_MAX, the algorithm would need to be reconsidered, though, since it's written with signed integers in mind. > Hopefully the proof would break if one tried to transfer it over? Hopefully. The proof would have to be modified to account for the actual types. If you're using bounded integers you'd need to write a different proof.
- derdi 1y ago> For UINT_MAX, the algorithm would need to be reconsidered, though, since it's written with signed integers in mind. The algorithm is written assuming that unary - produces the additive inverse. That is also true for C's unsigned integers. -1U == UINT_MAX, -UINT_MAX == 1U. It Just Works.
- junon 1y agoINT_MIN - 1 is undefined behavior in C.
- deleted 1y ago[deleted]
- zelphirkalt 1y agoWait, so much effort and it doesn't even consider this widely known issue? That would mean, that even though all this effort has been spent, a decent programmer still has a better idea of whether something is correct than the proof system used here. And worse this might lull one into thinking, that it must be correct, while actually for a simple case it breaks.
- Jtsummers 1y ago> a decent programmer still has a better idea of whether something is correct than the proof system used here. The proof is correct in the language it's written for, Lean. If you change the context (axioms) of a proof then the proof may be invalidated. This is not a surprising thing to anyone who spends a second thinking about it.
- Joker_vD 1y ago> anyone who spends a second thinking about it. Except most programmers don't spend even a second to think about it, and we end up with "int mid = (low + high) / 2;" bugs in standard implementations of binary search in e.g. Java. And that implementation even had a written proof accompanying it!
- Jtsummers 1y agoTry that in SPARK/Ada. It'll stop you there [if it can't prove that low + high won't overflow]. Don't take a proof written with one set of assumptions (in this case how integers are expected to behave) and translate it to another language where those assumptions don't hold.
- zelphirkalt 1y agoAre writing our next program in Lean then? Where does that run? There seems to be a fundamental difficulty here. Either we prove things in the language we want to use, which means modelling the behavior of the things we use in that language, or we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above. I would be surprised, if there was no standard approach for modelling bounded integers and their specific properties in a language (which can differ) in a proof language like this. There must have been more people having thought about this and come up with solutions.
- DavidVoid 1y ago> the algorithm will wrongfully report "false" for arrays like e.g. [INT_MIN, -1] If you have INT_MIN along with any other negative number in the array then your program has undefined behavior in C. Signed integer overflow is UB (but unsigned overflow is not).
- addaon 1y ago> If you have INT_MIN along with any other negative number in the array then your program has undefined behavior in C. What? Why? There’s no addition needed to solve this problem. The example implementation does invert each element, which is undefined for INT_MIN, but it would be trivial to just skip INT_MIN elements (since their additive inverse is never in the set).
- raphlinus 1y agoYes. The problem here is the -x operation. If INT_MIN is in the array, then the negation operation itself is UB. As you say, the fix is to skip values equal to INT_MIN; it's not possible that its negation is in the array, as that number is not representable. Rust is only a little better. With default settings, it will panic if isize::MIN is in the input slice in a debug build, and in a release build will incorrectly return true if there are two such values in the input. But in C you'll get unicorns and rainbows.
- andrepd 1y agoBut false is the correct result for those cases. Addition is addition and overflow is undefined (= can assume that doesn't happen), it's not addition modulo 2^n.
- Joker_vD 1y agoWe are not talking about C here. Imagine it was e.g. Java, or C#, or Rust in release mode, or heck, even Lean itself but with fixed-precision integers.
- alternatex 1y agoOverflow/underflow does happen in C# though. You have to manually opt-out by using a `checked` block anywhere you do arithmetic.
- necunpri 1y agoThis is the strength of typing, right? If I can specify the type of my input I can ensure the verification.
- sureglymop 1y agoHow so? If you specify the type int how would that save you from an overflow/underflow at runtime?
- alternatex 1y agoNot sure if types are supposed to protect against overflow/underflow, it's more in the arithmetic territory. Interesting idea though, I wonder if some programming language allows overflow/underflow checks directly in the types.
- Joker_vD 1y agoYes, it's actually quite easy: +: (int<N>, int<N>) -> int<N+1> // or (int<N>, bit) as the return type *: (int<N>, int<N>) -> int<2*N> etc. Those are the actual types of those arithmetic operations.
- ethan_smith 1y agoGood point about overflow - Lean can actually model machine integers with bounded arithmetic operations, allowing you to formally verify these edge cases by explicitly reasoning about overflow behavior.
- rck 1y agoDo you know of any short examples of this? Yesterday I was trying to prove some "easy" theorems that involved machine number representations, and I couldn't find anything in Lean.
- b0a04gl 1y ago[dead]
- munchler 1y agoLean is awesome and this is an impressive new feature, but I can't help but notice that the proof is significantly longer and more complex than the program itself. I wonder how well this will scale to real-world programs.
- grumbelbart 1y agoLong-term this would be done using LLMs. It would also solve LLMs' code quality issues - they could simply proof that the code works right.
- teiferer 1y ago[dead]
- codebje 1y agoMaybe very long term. I turn off code assistants when doing Lean proofs because the success rate for just suggestions is close to zero.
- photonthug 1y ago> simply proof that the code works right Combining LLMs + formal methods/model checkers is a good idea, but it's far from simple because rolling the dice on some subsymbolic stochastic transpiler from your target programming language towards a modeling/proving language is pretty suspect. So suspect in fact that you'd probably want to prove some stuff about that process itself to have any confidence. And this is a whole emerging discipline actually.. see for example https://sail.doc.ic.ac.uk/software/ https://sail.doc.ic.ac.uk/software/
- deleted 1y ago[deleted]
- amw-zero 1y agoResearch points to there being a quadratic relationship between automated proof and code size: https://trustworthy.systems/publications/nictaabstracts/Matichuk_MAJKS_15.abstract https://trustworthy.systems/publications/nictaabstracts/Mati.... Specifically, the relationship is between the _specification_ and the proof, and it was done for proofs written in Isabelle and not Lean. The good news is that more and more automation is possible for proofs, so the effort to produce each proof line will likely go down over time. Still, the largest full program we've fully verified is much less than 100,000 LOC. seL4 (verified operating system) is around 10,000 lines IIRC.
- norir 1y agoMy brain has been slowly trained to reject imperative programming. This example could be rewritten in a tail recursive manner using an immutable set which would be simpler to verify for correctness even without a formal verifier. I have found that while there is a learning curve to programming using only recursion for looping, code quality does go significantly up under this restriction. Here is why I personally think tail recursion is better than looping: with tail recursion, you are forced to explicitly reenter the loop. Right off the bat, this makes it difficult to inadvertently write an infinite loop. The early exit problem is also eliminated because you just return instead of making a recursive call. Moreover, using recursion generally forces you to name the function that loops which gives more documentation than a generic for construct. A halfway decent compiler can also easily detect tail recursion and rewrite it as a loop (and inline if the recursive function is only used in one place) so there need not to be any runtime performance cost of tail recursion instead of looping. Unfortunately many languages do not support tail call optimization or nested function definitions and also have excessively wordy function definition syntax which makes loops more convenient to write in those languages. This conditions one to think in loops rather than tail recursion. Personally I think Lean would be better if it didn't give in and support imperative code and instead helped users learn how to think recursively instead.
- kevindamm 1y agoWhich languages do support TCO at this point? From my recollection we have * Scheme * Haskell * Elixir * Erlang * OCaml * F# * Scala * (not Clojure) * the JVM could remove tail-recursive calls, but IIRC this still hasn't been added for security reasons * Racket * Zig * Lua * Common Lisp, under certain compilers/interpreters * Rust? (depends) * Swift? (sometimes)
- jeremyscanvic 1y agoThat's really neat! I'm very excited for the future of Lean.
- ryjo 1y agoVery cool. Neat how you managed to get logical symbols in to the language itself! When might someone use preconditions in Lean theorems? This article caught my eye because it's focused on imperative programming, and I've been very focused on declarative vs imperative programming over the last few years. I implemented a version of your function in CLIPS, a Rules-based language that takes a declarative approach to code: (defrule sum-is-0 (list $? ?first $? ?second $?) (test (= 0 (+ ?first ?second))) => (println TRUE)) (defrule sum-is-not-0 (not (and (list $? ?first $? ?second $?) (test (= 0 (+ ?first ?second))))) => (println FALSE)) (assert (list 1 0 2 -1)) (run) (exit) The theorem you write in Lean to prove the function kind-of exists in CLIPS Rules; you define the conditions that must occur in order to execute the Right Hand Side of the Rule. Note that the above simply prints `TRUE` or `FALSE`; it is possible to write imperative `deffunction`s that return values in CLIPS, but I wanted to see if I could draw parallels for myself between Lean code and theorems. Here's a gist with the simple version and a slightly more robust version that describes the index at which the matching numbers appear: https://gist.github.com/mrryanjohnston/680deaee87533dfedc74b461eef5a358 https://gist.github.com/mrryanjohnston/680deaee87533dfedc74b... Thank you for writing this and for your work on Lean! This is a concept that's been circling in my head for a minute now, and I feel like this article has unlocked some level of understanding I was missing before.
- drdeca 1y agoVery nice. However, I wonder whether it might be good to have a way to tell LEAN to spit out a more explicit form of the proof steps it obtained during `grind`? Like, to produce text for what one would put in there if one was doing it manually, that would work in place of grind, in case the grind step is slow to verify?
- yuppiemephisto 1y ago`show_term grind` and `by grind?` should do what you want
- bux93 1y agoIt looks suspiciously like verifying imperative code by writing declarative code that does the same thing.
- deleted 1y ago[deleted]