Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: "David MENTRÉ" <dmentre@linux-france.org>
To: caml-list@inria.fr
Subject: Re: [Caml-list] Program proof - how to do that?
Date: Sat, 19 Jul 2014 21:18:04 +0200	[thread overview]
Message-ID: <53CAC46C.2010905@linux-france.org> (raw)
In-Reply-To: <CAPFanBEuVWAxDHW4iMpoHU9JddzR46062c3EAjV9tX7L+8SmLw@mail.gmail.com>

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


  reply	other threads:[~2014-07-19 19:18 UTC|newest]

Thread overview: 8+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2014-07-12 11:25 Oliver Bandel
2014-07-12 11:56 ` Roberto Di Cosmo
2014-07-12 12:07 ` Gabriel Scherer
2014-07-19 19:18   ` David MENTRÉ [this message]
2014-07-21 22:37     ` Oliver Bandel
2014-07-22  8:25       ` Nuno Gaspar
2014-07-22 22:31         ` Oliver Bandel
2014-07-12 12:26 ` John Whitington

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=53CAC46C.2010905@linux-france.org \
    --to=dmentre@linux-france.org \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body. 
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox