[Haskell-cafe] Proving programs

[AUGER Cédric]

Le Tue, 01 Jan 2013 14:24:04 -0900,
Christopher Howard <christopher.howard at frigidcode.com> a écrit :

> I'm working through a video lecture describing how to prove programs
> correct, by first translating the program into a control flow
> representation and then using propositional logic. In the control flow
> section, the speaker described how the program should be understood in
> terms of an input vector (X, the inputs to the program), a program
> vector (Y, the storage variables), and an output vector (Z, the
> outputs of the program), with X mapping into Y, Y being affected by
> execution, and X and Y mapping into Z.
> 
> However, only part way into the video, two practical questions come
> to mind:
> 
> 1. Does this approach need to be adjusted for a functional language,
> in which computation is (at least idealistically) distinct from
> control flow?
> 
> 2. How do we approach this for programs that have an input loop (or
> recursion)? E.g., I have an application that reads one line for stdin,
> modifies said line, outputs to stdout, and repeats this process until
> EOF? Should I be thinking of every iteration as a separate program?
> 

Have you heard of Agda and Curry-Howard?

For imperative programs, you may also be interested in Hoare logic.

There are also some tools you may be interested in:
- Atelier B
- Why3

And probably many others.