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

61–70 of 105 posts

Re: My first verified imperative program

#61

Post by photonthug »

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.

> simply proof that the code works right

Combining LLMs + formal methods/model checkers is a good idea, but it's far from simple because rolling the dice on some subsymbolic stochastic transpiler from your target programming language towards a modeling/proving language is pretty suspect. So suspect in fact that you'd probably want to prove some stuff about that process itself to have any confidence. And this is a whole emerging discipline actually.. see for example https://sail.doc.ic.ac.uk/software/

Re: My first verified imperative program

#62

Post by addaon »

raphlinus wrote: post #55
addaon wrote: post #53

Earlier quoted context omitted.

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

> But in C you'll get unicorns and rainbows.

But in formally verified C you’ll have the algorithm that’s correct for that type (skip INT_MIN), or you won’t have a proof.

Re: My first verified imperative program

#63

Post by ryjo »

Very cool. Neat how you managed to get logical symbols in to the language itself! When might someone use preconditions in Lean theorems?

This article caught my eye because it's focused on imperative programming, and I've been very focused on declarative vs imperative programming over the last few years. I implemented a version of your function in CLIPS, a Rules-based language that takes a declarative approach to code:

(defrule sum-is-0 (list $? ?first $? ?second $?) (test (= 0 (+ ?first ?second))) => (println TRUE))

(defrule sum-is-not-0 (not (and (list $? ?first $? ?second $?) (test (= 0 (+ ?first ?second))))) => (println FALSE))

(assert (list 1 0 2 -1)) (run) (exit)

The theorem you write in Lean to prove the function kind-of exists in CLIPS Rules; you define the conditions that must occur in order to execute the Right Hand Side of the Rule. Note that the above simply prints `TRUE` or `FALSE`; it is possible to write imperative `deffunction`s that return values in CLIPS, but I wanted to see if I could draw parallels for myself between Lean code and theorems. Here's a gist with the simple version and a slightly more robust version that describes the index at which the matching numbers appear: https://gist.github.com/mrryanjohnston/680deaee87533dfedc74b...

Thank you for writing this and for your work on Lean! This is a concept that's been circling in my head for a minute now, and I feel like this article has unlocked some level of understanding I was missing before.

Re: My first verified imperative program

#64

Post by sureglymop »

necunpri wrote: post #36
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?

This is the strength of typing, right? If I can specify the type of my input I can ensure the verification.

How so? If you specify the type int how would that save you from an overflow/underflow at runtime?

Re: My first verified imperative program

#65

Post by drdeca »

Very nice. However, I wonder whether it might be good to have a way to tell LEAN to spit out a more explicit form of the proof steps it obtained during `grind`? Like, to produce text for what one would put in there if one was doing it manually, that would work in place of grind, in case the grind step is slow to verify?

Re: My first verified imperative program

#66

Post by Quekid5 »

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)

It's worth noting that some (many?) languages[0] only support TCO as long as you're calling the function itself in tail position. The usual cases were you'll notice this when implementing state machines in "direct style" or when doing continuation-passing style for control flow.

TCO is more general than that in some languages where any function call in tail position can be turned into a direct jump. This obviously requires either 1) runtime support in some form or 2) a non-trivial amount of program transformation during compilation.

[0] Scala's @tailrec is one I'm 100% certain of.

Re: My first verified imperative program

#67

Post by fc417fc802 »

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?

A language can provide arbitrary width integers while nonetheless being implemented on top of fixed width integers. In fact I'd say that's pretty typical.

Re: My first verified imperative program

#68

Post by tsimionescu »

lmm wrote: post #57
serbuvlad wrote: post #42

Earlier quoted context omitted.

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

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

No, it isn't, and yes, they would. The problem is that the terminal accepts certain valid UTF-8 characters (typically from the ASCII subset) as output control characters. This is how you get things like programs that can output colored text.

This is a part of the fundamental design of how a terminal device is supposed to work: its input is defined to be a single stream of characters, and certain characters (or sequences of characters) represent control sequences that change the way other characters are output. The problem here is with the design of POSIX in general and Linux in particular - the fact that, despite knowing most interaction will be done through a terminal device with no separate control and data channels, they chose to allow control characters as part of file names.

As a result of this, it is, by design, impossible to write a program that can print out any legal file name to a terminal without risking to put the terminal in a display state that the user doesn't expect. Best you could do is recognize terminal control sequences in file names, recognize if your output device is a terminal, and in those cases print out escaped versions of those character sequences.

Re: My first verified imperative program

#69

Post by fc417fc802 »

lmm wrote: post #57
serbuvlad wrote: post #42

Earlier quoted context omitted.

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

It's even worse than that. If a newer version of the compiler is able to leverage knowledge of the array bounds it could "optimize" away an entire chunk of your program. It probably won't do that because compiler authors supposedly aren't openly hostile towards compiler users but it isn't so easy to write an algorithm that will flag such "obviously" wrong things.

The control characters are themselves valid (but unprintable) UTF-8. They are also, against all common sense and reason, permitted within filenames by many filesystems. Rust won't save you here. https://www.compart.com/en/unicode/category/Cc

Re: My first verified imperative program

#70

Post by tsimionescu »

amw-zero wrote: post #26
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 like…

A small note, but seL4 is more of a kernel than a full OS - though in the embedded world for which it is targeted, the difference is pretty fuzzy.
Post reply on HN