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

My first verified imperative program

markushimmel.de

Post reply on HN
Print view View original

51–60 of 105 posts

Re: My first verified imperative program

#51

Post by rtpg »

munchler wrote: post #8

Lean 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.

My belief is that the core part of a lot of programs where you want formal proofs are tricky enough to where you need hand holding but the higher up the stack you go the simpler your proofs get since you did the hard stuff in the core.

Though it really does feel like we're still scratching the surface of proof writing practices. A lot of proofs I've seen seem to rely only on very low level building blocks, but stronger practitioners more immediately grab tools that make stuff simpler.

I would say, though, that it feels likely that your proofs are always going to be at least within an order of magnitude of your code, because in theory the longer your code is the more decision points there are to bring up in your proof as well. Though automatic proof searches might play out well for you on simpler proofs.

Re: My first verified imperative program

#52

Post by salutis »

kevindamm wrote: post #11
norir wrote: post #9

My 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 thin…

Which 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)

Also Fennel, both implicitly and explicitly with `tail!`.

Source: https://fennel-lang.org/reference#tail

Re: My first verified imperative program

#53

Post by addaon »

DavidVoid wrote: post #20
Joker_vD wrote: post #4

Naturally, 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?

> 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).

> 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).

Re: My first verified imperative program

#54

Post by buzzin_ »

norir wrote: post #9

My 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 thin…

I have found it that if you invest some time in learning how to write quality for loops, the quality indeed goes up.

Also, when writing for loops, you have to explicitly think about your exit condition for the loop, and it is visible right there, at the top of the loop, making infinite loops almost impossible.

Re: My first verified imperative program

#55

Post by raphlinus »

addaon wrote: post #53
DavidVoid wrote: post #20

Earlier quoted context omitted.

> 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).

> 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).

Yes. 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.

Re: My first verified imperative program

#56

Post by lmm »

Joker_vD wrote: post #22
Jtsummers wrote: post #13

Earlier quoted context omitted.

> 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.

> 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!

> 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!

I see this as far more of an indictment of Java than an indictment of programmers. If you make the symbol "+" part of your programming language's syntax (especially in a language where you don't allow custom implementations of "+") then it should do what the ordinary mathematical + operation does!

Re: My first verified imperative program

#57

Post by lmm »

serbuvlad wrote: post #42
armchairhacker wrote: post #33

Earlier quoted context omitted.

Real-world programs can be verified by formally proving properties on a small part of the code (called the kernel) in a way that transitively guarantees those for the remaining code. For example, Rust's borrow checker guarantees* memory safety of any code written in Rust, even a 10M+ LOC project. Another example is sel4, a formally-verified micro-kernel ( https://sel4.systems/About/seL4-whitepaper.pdf ). * Technicall…

What's a memory issue? If I access beyond the end of an array in Rust, the panic handler runs and starts unwinding my stack. If I access beyond the end of an array in C++ with .at() the excwption handler runs and starts unwining my stack. If I access beyond the end of an array in C the SIGSEGV handler may (*) run and I could, if I wanted to, start unwinding my stack. Ah, but in C, sometimes if I access the wrong memo…

> Sure, and if I store my data in a Rust array and store indexes into that array around the place as sort of weak references (something I've seen Rust programmers use and talk about all the time), I can easily fetch the wrong data too.

Maybe, but you'll do so in an understandable way that you can catch in testing. You won't suddenly start fetching different wrong data when someone builds your program with a newer version of the compiler, which is a very real risk with C. To say nothing of the risk of arbitrary code execution if your program is operating on attacker-supplied data.

> The irony, of couse, is that the characters that can break your terminal session are perfectly valid UTF-8.

Terminals that can't handle the full UTF-8 range are a problem with those terminals IMO. And terminals implemented in Rust probably don't have that problem :).

Re: My first verified imperative program

#58

Post by MobiusHorizons »

Jtsummers wrote: post #43
zelphirkalt wrote: post #37

Earlier quoted context omitted.

Are 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…

> Are writing our next program in Lean then? Where does that run? That first question is hard to parse. If you mean "Are you writing your next program in Lean then?" then: No, but in principle we could, it runs on each OS we use (Windows and Linux, standard x64 hardware). If you mean something else, I can't figure out what it would be. > Either we prove things in the language we want to use Sure, I mentioned SPARK/Ad…

What hardware doesn’t use fixed width integers?

Re: My first verified imperative program

#59

Post by Jtsummers »

MobiusHorizons wrote: post #58
Jtsummers wrote: post #43

Earlier quoted context omitted.

> Are writing our next program in Lean then? Where does that run? That first question is hard to parse. If you mean "Are you writing your next program in Lean then?" then: No, but in principle we could, it runs on each OS we use (Windows and Linux, standard x64 hardware). If you mean something else, I can't figure out what it would be. > Either we prove things in the language we want to use Sure, I mentioned SPARK/Ad…

What hardware doesn’t use fixed width integers?

What's the context of your question? Did I say otherwise?

Some languages (what's being discussed here) give you arbitrary precision integers, like Lean. So the proof in the blog applies to Lean and any issues with things like -INT_MIN not existing isn't a factor in the proof. That's what's being discussed. The proof for C or Ada or something else with fixed-width integers will be different (and the algorithm, likely) to account for that difference and any other relevant differences.

Post reply on HN