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

41–50 of 105 posts

Re: My first verified imperative program

#41

Post by Joker_vD »

andrepd wrote: post #34
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?

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

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

Re: My first verified imperative program

#42

Post by serbuvlad »

armchairhacker wrote: post #33
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.

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 memory, I get garbadge instead of a panic.

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.

Rust provides a robust type system and a borrow checker which avoids a lot of common problems at the expence of adhering to a particular programming style. That's fine. That's worth advocating for.

But it's no pannacea. Not even close.

My favorite memory about this is a programmer lambasting Go's strings (which are basically immutable byte vectors) for not enforcing UTF-8, like Rust strings.

He then said that this means that in Go you can print filenames to the screen that can break your terminal session because of this if they contain invalid UTF-8, which Rust forces you to escape explicitly. The irony, of couse, is that the characters that can break your terminal session are perfectly valid UTF-8.

Rust's type safety convinced this guy that his Rust program was immune to a problem that it was simply not immune to.

Re: My first verified imperative program

#43

Post by Jtsummers »

zelphirkalt wrote: post #37
Jtsummers wrote: post #23

Earlier quoted context omitted.

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.

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/Ada. There are systems for C, Java, and others that also work and understand their types so you don't have to add extra modeling.

> which means modelling the behavior of the things we use in that language

It would already be done for you, you wouldn't have to model Ada's integers in SPARK, for instance.

> we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above.

https://lean-lang.org/doc/reference/latest/Basic-Types/Fixed...

If you knew your target system was using fixed-width integers, you'd use this.

Re: My first verified imperative program

#44

Post by codebje »

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.

Maybe very long term. I turn off code assistants when doing Lean proofs because the success rate for just suggestions is close to zero.

Re: My first verified imperative program

#45

Post by aseipp »

zelphirkalt wrote: post #37
Jtsummers wrote: post #23

Earlier quoted context omitted.

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.

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…

It does not look like it due to its largest target audience (hardcore math nerds writing proofs), but Lean 4 is actually a meta-programming language, like Racket -- it is one single unified language for programming, meta programming, and theorem proving, on top of a small core. The implementation of Lean is almost entirely written in Lean, including components like LSP servers, the compiler itself, many efficient data structures, etc. It is a key use case to write real world programs, because the implementation itself is such a program.

In the long past, Lean 3 had this idea that you could use one language both for writing proofs, and writing proof automation -- programs that manipulate proofs and automatically do things. Like in the article itself, the 'grind' thing-a-mabob is proof automation. (Roqc has two separate languages for proofs and proof automation.) But there was a problem: Lean started as a theorem prover and the implementation tried to move towards "executing programs" and it didn't work very well and was slow. The prototype compiler from Lean 3 to C++ ran out of steam before Lean 3 got canned.

Lean 4 instead went and did things the other way around: it started as a programming language that was executable. The Lean 4 compiler was self-hosted during development for a long-time, way before anyone ported any big math proofs to it from Lean 3. Why did they do this? Because the key insight is that if you want to write programs that manipulate proofs (AKA programs), the best thing to have at hand is have a robust general programming language -- like Lisp or Racket. And so Lean is macro based, too, and like Racket it allows you to have families of languages and towers of macros that expand as deep as you want. Meta programs that write programs that write programs, etc...

So in Lean you write Lean programs that can manipulate Lean ASTs, and you write "reader macros" that allow you to use domain specific syntax right inside the source file for any kind of math or programming-language DSL you want. And all those macros and meta-programs are compiled and executed efficiently just like you'd expect. Finally, there is a total fragment of the language that you can actually write proofs over and reason about. And there is a big library called "mathlib" with lots of macros for writing math and math proofs in this language-framgent-we-can-reason-and-prove-things-with.

Lean 4 is very close in spirit to the Lisp idea, but modified for math proving and generalized programming. It's very unique and powerful.

Re: My first verified imperative program

#46

Post by tuveson »

taeric wrote: post #27
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…

> I've certainly messed up my fair share of recursive calls.

It’s a common enough problem that the “why is my program crashing” website is basically named after it.

Re: My first verified imperative program

#47

Post by junon »

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…

INT_MIN - 1 is undefined behavior in C.

Re: My first verified imperative program

#48

Post by [deleted] »

junon wrote: post #47
Jtsummers wrote: post #6

Earlier quoted context omitted.

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

INT_MIN - 1 is undefined behavior in C.

[deleted]

Re: My first verified imperative program

#49

Post by geoffhill »

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)

Both Clang and GCC have musttail attributes than can force tail calls at specific return statements in C/C++.

Re: My first verified imperative program

#50

Post by caim »

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…

Funny thing is that you can get undefined behavior and segfaults using only "safe rust", and the rust compiler has subtle bugs that allow you to disable important checks (like type checking), which can leave your code completely broken.

But for some crazy propaganda, rust devs believes that any rust code is safe and sound no matter what.

https://github.com/Speykious/cve-rs/issues/49

Post reply on HN