From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <dmentre@linux-france.org>
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 062527FA4D
	for <caml-list@sympa.inria.fr>; Sat, 19 Jul 2014 21:18:06 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  dmentre@linux-france.org) identity=pra;
  client-ip=94.23.39.64;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="dmentre@linux-france.org";
  x-sender="dmentre@linux-france.org";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  dmentre@linux-france.org) identity=mailfrom;
  client-ip=94.23.39.64;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="dmentre@linux-france.org";
  x-sender="dmentre@linux-france.org";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@tempura.bentobako.org) identity=helo;
  client-ip=94.23.39.64;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="dmentre@linux-france.org";
  x-sender="postmaster@tempura.bentobako.org";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AvUHAP7DylNeFydA/2dsb2JhbABZgw5SWIJ3whaHQgGBBxZ2hAQBBSMVQBELGgIFFgsCAgkDAgECAQ04EwgBAYhCCasKlyAXgSyOJhaCYoFOAQSOQ4INjCKFSI0ag0Y
X-IPAS-Result: AvUHAP7DylNeFydA/2dsb2JhbABZgw5SWIJ3whaHQgGBBxZ2hAQBBSMVQBELGgIFFgsCAgkDAgECAQ04EwgBAYhCCasKlyAXgSyOJhaCYoFOAQSOQ4INjCKFSI0ag0Y
X-IronPort-AV: E=Sophos;i="5.01,692,1400018400"; 
   d="scan'208";a="72090081"
Received: from tempura.bentobako.org ([94.23.39.64])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 19 Jul 2014 21:18:06 +0200
Received: from [192.168.0.50] (85-171-113-17.rev.numericable.fr [85.171.113.17])
	by tempura.bentobako.org (Postfix) with ESMTPSA id AECFD16D1
	for <caml-list@inria.fr>; Sat, 19 Jul 2014 21:18:04 +0200 (CEST)
Message-ID: <53CAC46C.2010905@linux-france.org>
Date: Sat, 19 Jul 2014 21:18:04 +0200
From: =?UTF-8?B?RGF2aWQgTUVOVFLDiQ==?= <dmentre@linux-france.org>
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0
MIME-Version: 1.0
To: caml-list@inria.fr
References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> <CAPFanBEuVWAxDHW4iMpoHU9JddzR46062c3EAjV9tX7L+8SmLw@mail.gmail.com>
In-Reply-To: <CAPFanBEuVWAxDHW4iMpoHU9JddzR46062c3EAjV9tX7L+8SmLw@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Program proof - how to do that?

Hello Gabriel,

2014-07-12 14:07, Gabriel Scherer:
> I tried to (partially) answer this question in the following
> StackOverflow thread:
>    http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations


Nice answer.

BTW, regarding Why3 in your answer, the current git version of Why3 
allows to produce OCaml code from a proved WhyML program, thus allowing 
production of certified OCaml code (like with Coq but using Deductive 
Verification approach and automated provers). This is currently Work In 
Progress and actively developed but this feature will be definitely be 
part of the next stable release of Why3 (and you can already play with 
it by compiling the git version).

Best regards,
david