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

21–30 of 105 posts

Re: My first verified imperative program

#21

Post by derdi »

Jtsummers wrote: post #6
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] `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…

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

Re: My first verified imperative program

#22

Post by Joker_vD »

Jtsummers wrote: post #13
zelphirkalt wrote: post #10

Earlier quoted context omitted.

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

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

Re: My first verified imperative program

#23

Post by Jtsummers »

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!

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

Re: My first verified imperative program

#25

Post by alexisread »

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)

Freeforth (implicit) and Ableforth (deliberately explicit)

Re: My first verified imperative program

#26

Post by amw-zero »

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.

Research points to there being a quadratic relationship between automated proof and code size: 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.

Re: My first verified imperative program

#27

Post by taeric »

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…

This feels overly strong? I've certainly messed up my fair share of recursive calls.

I don't know why, but I have actually gotten a bit stronger on the imperative divide in recent years. To the point that I found writing, basically, a GOTO based implementation of an idea in lisp to be easier than trying to do it using either loops or recursion. Which, really surprised me.

I /think/ a lot of the difference comes down to how localized the thinking is. If I'm able to shrink the impact of what I want to do down to a few arguments, then recursion helps a ton. If I'm describing a constrained set of repetitive actions, loops. If I'm trying to hold things somewhat static as I perform different reduction and such, GOTO works.

I think "functional" gets a bit of a massive boost by advocates that a lot of functional is presented as declarative. But that doesn't have to be the case. Nor can that help you, if someone else hasn't done the actual implementation.

We can get a long way with very mechanical transformations, in the form of compilation. But the thinking can still have some very imperative aspects.

Re: My first verified imperative program

#28

Post by taeric »

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)

I don't understand the security reasons on not removing tail calls. Any chance you have a good place to read up on that?

Re: My first verified imperative program

#30

Post by teiferer »

grumbelbart wrote: post #19
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.

Long-term this would be done using LLMs. It would also solve LLMs' code quality issues - they could simply proof that the code works right.

[dead]
Post reply on HN