what does it mean to prove the correctness of a program?

Stream: Program verification

[Bulhwi Cha]

For example, what exactly does it mean to prove the correctness of the following Lean program, HelloName.lean? How do I do that?

def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace

  stdout.putStrLn s!"Hello, {name}!"

[Henrik Böving]

You provide a specification and then you need to verify that specification. without specification there is nothing to be done.

[Bulhwi Cha]

What would be a specification of the HelloName.lean program? What theorems should I prove? I haven't started learning about program verification, so it's been difficult for me to imagine what a specification of a program would look like.

[Henrik Böving]

"Name contains no white spaces on the right", " name is only alpha numeric " (you violate that), "the program always asks for input before giving output". Many specifications are possible.

[Bulhwi Cha]

I see. I don't know how one can state in Lean that the program always asks for input before giving output, but I guess there's a way for it.

[Chris Bailey]

Bulhwi Cha said:

What would be a specification of the HelloName.lean program? What theorems should I prove? I haven't started learning about program verification, so it's been difficult for me to imagine what a specification of a program would look like.

I think this is not an exciting example if you're starting to explore verification; it mostly concerns IO and related side effects which are necessarily opaque in Lean and don't permit very robust specifications or feats of verification in userspace. The hitchhikers guide and software foundations (second half of vol 1, and vol 2) have pretty reasonable introductions to verification of basic imperative programs.

[Yves Jäckle]

Maybe one could use a state monad transformer who's state can be used for tracing, then add state changes after the IO actions, and finally prove that the trace has the order in which stdin occurred before stdout ?
The same could work for a runtime analysis. Every time you perform an elementary operation, you increase the counter in the state. Then, you prove the big-oh stuff for that counter.
I'm no expert though. Hope someone posts an example in this thread. I would love to see the API of Batteries.Control for example in action.

[Bulhwi Cha]

Chris Bailey said:

I think this is not an exciting example if you're starting to explore verification; it mostly concerns IO and related side effects which are necessarily opaque in Lean and don't permit very robust specifications or feats of verification in userspace.

For these reasons, I think proof-oriented programming languages like F* and Dafny currently offer better support for verification of effectful programs.

[Chris Bailey]

I don't think those necessarily get you much further in this case; the boundaries of what behavior or properties you can claim are verified depends on whether or not you have a model of what the host machine does with IO. You can lift certain properties into Lean and reason about them, which is what Yves suggested, ultimately you have to hand the results off to the computer.

It's possible to specify and reason about what the operating system does with the end result, I think that's what the Coq ecosystem's "verified software toolchain" is about, and I assume the sel4 proofs include stuff like this, but my understanding is that it's a question of having those libraries and tools that know about and describe the compiler, operating system, etc available, not whether the type theory or effect system has a certain feature.

[Bulhwi Cha]

Chris Bailey said:

…, but my understanding is that it's a question of having those libraries and tools that know about and describe the compiler, operating system, etc available, not whether the type theory or effect system has a certain feature.

I agree. It's a question of whether libraries and tools for certain work are currently available to a language's ecosystem.

[Ira Fesefeldt]

I'd like to add that for specifications of the sort "The program always asks for input before giving output" you also likely need some sort of temporal logic, which - as far as I know - is rare outside of model checkers. Lean, Dafny and the like shine for functional specifications.

[Hz]

I think the use case of an ERC20 smart contract, where the total supply must be always the sum of all balances is a good property to think about a program. That's is done in dafny like this https://github.com/Consensys/WrappedEther.dfy/blob/main/src/WrappedEtherModel.dfy

[pandaman]

One thing you can do is to write your effectful program in the sans-IO style. This method involves implementing the protocol as pure functions representing a state machine with inputs/outputs. Then you create another layer that wires actual IO to the state machine.
While it remains hard to verify the wiring layer for reasons discussed here, you can get far by verifying the state machine, and it's no different from other Lean proofs since it's just pure functions.

[Julian Berman]

sans-IO is great, it'd be awesome if it were 87 times more popular in the (Python) ecosystem than it already is, but I have never seen something that was a non "traditional-IO-protocoly" thing (e.g. an HTTP server, a client for some REST API, PROXY protocol, bla bla...) be written specifically claiming to be a "sans-IO program". (I'm not sure what the point of my comment is, only that it's interesting that you brought up sans-IO in this context, and maybe it indeed would be nice to somehow have the sans-IO docs relate to the point you were making)

[Julian Berman]

Though I guess e.g. Gary Bernhardt's "Functional Core, Imperative Shell" (https://www.destroyallsoftware.com/screencasts/catalog/functional-core-imperative-shell) or just generally the adage to separate logic from state is already quite similar.

[pandaman]

Yeah, I would say these more or less refer to the same concept in a sense that purity helps understanding/testing/verification/etc. I brought up sans-IO here because this particular example sounds a bit like an interactive message protocol.

[Michal Wallace (tangentstorm)]

I am fond of Eric Hehner's way of thinking (from aPToP and the corresponding video course:

• a specification of behavior is just a big binary (boolean) expression relating an initial state of a system to a resulting state
• some specifications are implementable, some are not (ex: you can't specify what the input will be. you can only specify what the output will be given a certain input)
• of the implementable specifications, some are directly executable
• for those that aren't, you can implement them by refining the specification until the whole thing is directly executable
• a program is a specification of behavior that is directly executable

In the case of Lean, the specification language includes a syntax for describing which things happen before which other things... So in Lean, your code is already a specification that the input happens before the output.

You don't need to prove a specification that are directly executable. (What is there to prove? That the spec is the spec?) (You could talk about a proof that the lean compiler correctly generates the machine for the program you wrote, but then you're verifying lean, not your program.)

OTOH, if you were using a more complicated algorithm with multiple threads or some other abstraction so that the order of execution was no longer directly specified in the code, then it might make sense to prove statements about the order of operations.

[Michal Wallace (tangentstorm)]

FWIW, I'm not an expert at this, but I've been working to formally specify what a "prime number sieve" is and verify that a particular algorithm implements that spec in lean for the past few weeks, and keeping a dev log in this thread.

[Chris Bailey]

Ira Fesefeldt said:

I'd like to add that for specifications of the sort "The program always asks for input before giving output" you also likely need some sort of temporal logic, which - as far as I know - is rare outside of model checkers. Lean, Dafny and the like shine for functional specifications.

I don't think you need to reach for temporal logic. You can either appeal to the evaluation order of the language (for putStrLn (f getInput) under eager evaluation , f getInput will be evaluated before putStrLn), or you can assign the result of getInput to a variable Option String that starts as None and state that the output operation only succeeds if the variable has been assigned/is not None.

[Ira Fesefeldt]

Chris Bailey said:

I don't think you need to reach for temporal logic. You can either appeal to the evaluation order of the language (for putStrLn (f getInput) under eager evaluation , f getInput will be evaluated before putStrLn), or you can assign the result of getInput to a variable Option String that starts as None and state that the output operation only succeeds if the variable has been assigned/is not None.

Maybe this is a philosophical question, but I do think you only proved a specification if there is a theorem that states the specification clearly and is correct. And I don't see how any of these solutions is able to specify the property in a theorem? It looks to me like software engineering patterns that guarantee you the specification, but doesn't give you the possibility to actually prove the correctness of the specification? But I may also misunderstand you.

[Chris Bailey]

Ira Fesefeldt said:

Chris Bailey said:

I don't think you need to reach for temporal logic. You can either appeal to the evaluation order of the language (for putStrLn (f getInput) under eager evaluation , f getInput will be evaluated before putStrLn), or you can assign the result of getInput to a variable Option String that starts as None and state that the output operation only succeeds if the variable has been assigned/is not None.

Maybe this is a philosophical question, but I do think you only proved a specification if there is a theorem that states the specification clearly and is correct. And I don't see how any of these solutions is able to specify the property in a theorem? It looks to me like software engineering patterns that guarantee you the specification, but doesn't give you the possibility to actually prove the correctness of the specification? But I may also misunderstand you.

If temporal logic is on the table and we're assuming there's a defined semantics available, I don't think it's controversial to reason that because a program P which references a variable x can make progress iff x is defined when it's referenced, termination of a program x := readInput; putStrLn x is a valid proof that readInput was executed before putStrLn. I agree that whether the addition of temporal logic would add a more helpful notion of "before" is a matter of opinion.

[Tyler Josephson ⚛️]

Ira Fesefeldt said:

Chris Bailey said:

I don't think you need to reach for temporal logic. You can either appeal to the evaluation order of the language (for putStrLn (f getInput) under eager evaluation , f getInput will be evaluated before putStrLn), or you can assign the result of getInput to a variable Option String that starts as None and state that the output operation only succeeds if the variable has been assigned/is not None.

Maybe this is a philosophical question, but I do think you only proved a specification if there is a theorem that states the specification clearly and is correct. And I don't see how any of these solutions is able to specify the property in a theorem? It looks to me like software engineering patterns that guarantee you the specification, but doesn't give you the possibility to actually prove the correctness of the specification? But I may also misunderstand you.

Can someone say “my specification is that my recursive function must halt” and Lean confirms that? Would this be part of program verification, even though no theorem is stated? Or does this not count?

[Ira Fesefeldt]

Termination is special as it is hard coded into lean - the missing partial keyword is the specification that the function terminates. And at least I would count that as a valid specification. And that's definitely program verification.

[Henrik Böving]

Tyler Josephson ⚛️ said:

Ira Fesefeldt said:

Chris Bailey said:

I don't think you need to reach for temporal logic. You can either appeal to the evaluation order of the language (for putStrLn (f getInput) under eager evaluation , f getInput will be evaluated before putStrLn), or you can assign the result of getInput to a variable Option String that starts as None and state that the output operation only succeeds if the variable has been assigned/is not None.

Maybe this is a philosophical question, but I do think you only proved a specification if there is a theorem that states the specification clearly and is correct. And I don't see how any of these solutions is able to specify the property in a theorem? It looks to me like software engineering patterns that guarantee you the specification, but doesn't give you the possibility to actually prove the correctness of the specification? But I may also misunderstand you.

Can someone say “my specification is that my recursive function must halt” and Lean confirms that? Would this be part of program verification, even though no theorem is stated? Or does this not count?

Most program verification that is done irl right now relies on completely unverified tools to basically say "yes it's fine" or "no, here is a counter example" (sometimes without the counter example part). Not having a theorem in Lean stated but having the thing otherwise verified by Lean is a perfectly fine notion of verification^^