From: "David MENTRÉ" <david.mentre@bentobako.org>
To: caml-list@inria.fr
Subject: Re: [Caml-list] FoCaLiZe 0.9.2 released
Date: Mon, 3 Sep 2018 18:02:26 +0200 [thread overview]
Message-ID: <30e39671-f6a3-cbd5-284e-ed23d4456adf@bentobako.org> (raw)
In-Reply-To: <1C15EE94-097B-4758-815F-1F9D0BB5EF6C@ensta.fr>
Hello François Pessaux,
Le 03/09/2018 à 10:38, François Pessaux a écrit :
> The FoCaLiZe system provides means for the developers to formally express
> their specifications and to go step by step (in an incremental approach) to
> design and implementation, while proving that their implementation
> meets its specification or design requirements. The FoCaLiZe language offers
> high level mechanisms such as inheritance, late binding, redefinition,
> parametrization, etc. Confidence in proofs submitted by developers or
> automatically generated ultimately relies on Coq formal proof verification.
A maybe naive question: what are the distinguishing points of Focalize
compared to Coq, Isabelle, F* or B Method? For which fundamental reason
I should use Focalize instead of other tool to develop high integrity
programs or systems? I read the "What is it FoCaLiZe ?" section but for
me it does not answer my question.
You can reply to me privately if you think this is inappropriate for
caml-list.
Best regards,
D. Mentré
--
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
next prev parent reply other threads:[~2018-09-03 16:03 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <A04F917F-3FD5-42AD-BF41-61D2A4DC7A4A@ensta.fr>
2018-09-03 8:38 ` François Pessaux
2018-09-03 16:02 ` David MENTRÉ [this message]
2018-09-03 17:06 ` Serge Le Huitouze
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=30e39671-f6a3-cbd5-284e-ed23d4456adf@bentobako.org \
--to=david.mentre@bentobako.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;
as well as URLs for NNTP newsgroup(s).