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

[Roberto Di Cosmo <roberto@dicosmo.org>]

Dear Oliver,
     there have been decades of research going on on all this,
and it would be kind of pretentious to try and sum them up
in a few lines here.

Let me offer a suggestion nonetheless: if you happen to be near Vienna in
the very next days, you should definitely go and attend some of the talks that
will take place in the Vienna Summer of Logic 2014 event (http://vsl2014.at/)

There will be tracks on hardware verification, software verification,
theorem proving, logic and all that :-)

--
Roberto


On Sat, Jul 12, 2014 at 01:25:48PM +0200, 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.
> 
> 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

-- 
Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 3020 (3rd floor)
Batiment Sophie Germain
Avenue de France
Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
-----------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3