From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <john@coherentgraphics.co.uk>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id CFE167FA1F
	for <caml-list@sympa.inria.fr>; Sat, 12 Jul 2014 14:26:42 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  john@coherentgraphics.co.uk) identity=pra;
  client-ip=188.64.184.40;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="john@coherentgraphics.co.uk";
  x-sender="john@coherentgraphics.co.uk";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  john@coherentgraphics.co.uk) identity=mailfrom;
  client-ip=188.64.184.40;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="john@coherentgraphics.co.uk";
  x-sender="john@coherentgraphics.co.uk";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@bluechip4.ukhost4u.com) identity=helo;
  client-ip=188.64.184.40;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="john@coherentgraphics.co.uk";
  x-sender="postmaster@bluechip4.ukhost4u.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgABADsowVO8QLgoemdsb2JhbABZg2CDS75Ih0cBgQ4WDwEBCwcNCTyEAwEBBSMVQAEQCwcRAgIFFgsCAgkDAgECAUUGDohLAa5BmCkXgSyNR1gHgneBTAEEoiGQT4Ft
X-IPAS-Result: AgABADsowVO8QLgoemdsb2JhbABZg2CDS75Ih0cBgQ4WDwEBCwcNCTyEAwEBBSMVQAEQCwcRAgIFFgsCAgkDAgECAUUGDohLAa5BmCkXgSyNR1gHgneBTAEEoiGQT4Ft
X-IronPort-AV: E=Sophos;i="5.01,649,1400018400"; 
   d="scan'208";a="71182005"
Received: from bluechip4.ukhost4u.com ([188.64.184.40])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 12 Jul 2014 14:26:41 +0200
Received: from [46.64.58.87] (port=63167 helo=[192.168.1.175])
	by bluechip4.ukhost4u.com with esmtpsa (TLSv1:DHE-RSA-CAMELLIA256-SHA:256)
	(Exim 4.82)
	(envelope-from <john@coherentgraphics.co.uk>)
	id 1X5wNz-0035eM-Rp; Sat, 12 Jul 2014 13:26:39 +0100
Message-ID: <53C1297B.4030806@coherentgraphics.co.uk>
Date: Sat, 12 Jul 2014 13:26:35 +0100
From: John Whitington <john@coherentgraphics.co.uk>
User-Agent: Postbox 3.0.11 (Macintosh/20140602)
MIME-Version: 1.0
To: Oliver Bandel <oliver@first.in-berlin.de>
CC: caml-list@inria.fr
References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de>
In-Reply-To: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
X-AntiAbuse: This header was added to track abuse, please include it with any abuse report
X-AntiAbuse: Primary Hostname - bluechip4.ukhost4u.com
X-AntiAbuse: Original Domain - inria.fr
X-AntiAbuse: Originator/Caller UID/GID - [47 12] / [47 12]
X-AntiAbuse: Sender Address Domain - coherentgraphics.co.uk
X-Get-Message-Sender-Via: bluechip4.ukhost4u.com: authenticated_id: john@coherentgraphics.co.uk
Subject: Re: [Caml-list] Program proof - how to do that?

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/