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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

I tried to (partially) answer this question in the following
StackOverflow thread:
  http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations



On Sat, Jul 12, 2014 at 1:25 PM, Oliver Bandel
<oliver@first.in-berlin.de> 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.
>
> Ciao,
>    Oliver
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs