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

11–20 of 105 posts

Re: My first verified imperative program

#11

Post by kevindamm »

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)

Re: My first verified imperative program

#12

Post by louthy »

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 agree, but also folds, traversals, list-comprehensions, and recursion-schemes work well and can be even more resistent to common bugs than regular recursion.

Although it’s hard to fault the simple elegance of recursion!

Re: My first verified imperative program

#13

Post by Jtsummers »

zelphirkalt wrote: post #10
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?

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.

Re: My first verified imperative program

#14

Post by louthy »

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)

> * F#

The .NET CLR supports the ‘.tail’ opcode which means that any .NET based language could support it. I’m hoping one day the C# team will get around to it. It seems like such low hanging fruit.

Re: My first verified imperative program

#15

Post by nhubbard »

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)

Kotlin as well, through the ‘tailrec’ marker on a function.

Re: My first verified imperative program

#16

Post by kevindamm »

nhubbard wrote: post #15
kevindamm wrote: post #11

Earlier quoted context omitted.

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)

Kotlin as well, through the ‘tailrec’ marker on a function.

ah, thanks, good to know.. but does that make it optional? I kind of like how ocaml requires a letrec annotation on any recursive definition and I don't know when you wouldn't want to add tailrec

Re: My first verified imperative program

#18

Post by [deleted] »

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…

[deleted]

Re: My first verified imperative program

#19

Post by grumbelbart »

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.

Re: My first verified imperative program

#20

Post by DavidVoid »

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

Post reply on HN