My first verified imperative program
markushimmel.de
My first verified imperative program
1–10 of 105 posts
Re: My first verified imperative program
#2[deleted]
Re: My first verified imperative program
#3[deleted]
[deleted]
Re: My first verified imperative program
#4Naturally, 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?
Re: My first verified imperative program
#5nice
Re: My first verified imperative program
#6Naturally, 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 using bounded integers you'd need to write a different proof.
Re: My first verified imperative program
#7[dead]
Re: My first verified imperative program
#8Lean 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.
Re: My first verified imperative program
#9My 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.
Re: My first verified imperative program
#10Naturally, 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?
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.