From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oliver@first.in-berlin.de>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 22F9E7FA1F
	for <caml-list@sympa.inria.fr>; Sat, 12 Jul 2014 13:25:52 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  oliver@first.in-berlin.de) identity=pra;
  client-ip=192.109.42.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oliver@first.in-berlin.de";
  x-sender="oliver@first.in-berlin.de";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  oliver@first.in-berlin.de) identity=mailfrom;
  client-ip=192.109.42.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oliver@first.in-berlin.de";
  x-sender="oliver@first.in-berlin.de";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@einhorn.in-berlin.de) identity=helo;
  client-ip=192.109.42.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oliver@first.in-berlin.de";
  x-sender="postmaster@einhorn.in-berlin.de";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AqwAAPoZwVPAbSoInGdsb2JhbABZhDqCccceFg8BAQEBAQgLCQkUKIQtFXYCGA4CiTQEnxWPI5hIgSyNR3WCYTaBFgWbDYcPizaFH4Fs
X-IPAS-Result: AqwAAPoZwVPAbSoInGdsb2JhbABZhDqCccceFg8BAQEBAQgLCQkUKIQtFXYCGA4CiTQEnxWPI5hIgSyNR3WCYTaBFgWbDYcPizaFH4Fs
X-IronPort-AV: E=Sophos;i="5.01,649,1400018400"; 
   d="scan'208";a="84905379"
Received: from einhorn.in-berlin.de ([192.109.42.8])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 12 Jul 2014 13:25:51 +0200
X-Envelope-From: oliver@first.in-berlin.de
X-Envelope-To: <caml-list@inria.fr>
Received: from yak (yak.in-berlin.de [192.109.42.109])
	by einhorn.in-berlin.de (8.14.4/8.14.4/Debian-4) with ESMTP id s6CBPnae018126
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT)
	for <caml-list@inria.fr>; Sat, 12 Jul 2014 13:25:49 +0200
Received: from e178027047.adsl.alicedsl.de (e178027047.adsl.alicedsl.de
 [85.178.27.47]) by webmail.in-berlin.de (Horde Framework) with HTTP; Sat, 12
 Jul 2014 13:25:48 +0200
Date: Sat, 12 Jul 2014 13:25:48 +0200
Message-ID: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de>
From: Oliver Bandel <oliver@first.in-berlin.de>
To: caml-list@inria.fr
User-Agent: Internet Messaging Program (IMP) H5 (6.2.0)
Content-Type: text/plain; charset=UTF-8; format=flowed; DelSp=Yes
MIME-Version: 1.0
Content-Disposition: inline
Subject: [Caml-list] Program proof - how to do that?

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