Re: [Caml-list] Program proof - how to do that?

[John Whitington <john@coherentgraphics.co.uk>]

Hi,

Oliver Bandel wrote:
> Hello,
>
> how can program proof be done in the real world?
> What are the theoretical things needed to know?
> And how to bring together the theory and the practise?
>
> During the last some months I looked into how mathematical
> proof works, and how natural deduction works (also looked at calculus
> for natural deduction).
>
> How can this be used in the real world of (OCaml-)programming
> to make a proof on the functionality of software?
>
> There seem to be limits coming from the halting problem,
> but AFAIK with a reduced set of operations, then in this
> limited set of instructions, this problem can be circumvented.
> What are the details on this topic? What kind of operations
> can be proofed to be safe (doing what is intended),
> and which (kind of) operations would not be possible to
> become proofed?
>
> Any explanation as well as hints on literature are welcome.

Chapter 6 ("Reasoning About Functional Programs"), of Paulson's "ML for 
the Working Programmer", is a very gentle introduction to this kind of 
thing.

Thanks,

-- 
John Whitington
Director, Coherent Graphics Ltd
http://www.coherentpdf.com/