* [Caml-list] FoCaLiZe 0.9.2 released [not found] <A04F917F-3FD5-42AD-BF41-61D2A4DC7A4A@ensta.fr> @ 2018-09-03 8:38 ` François Pessaux 2018-09-03 16:02 ` David MENTRÉ 0 siblings, 1 reply; 3+ messages in thread From: François Pessaux @ 2018-09-03 8:38 UTC (permalink / raw) To: caml-list [-- Attachment #1: Type: text/plain, Size: 3747 bytes --] It is my pleasure to announce the new release for FoCaLiZe (the 0.9.2 version). As for previous releases, some bugs have been fixed in the focalizec compiler. This version introduces the Dedukti backend written by Raphaël Cauderlier, taking benefits from Zenon_modulo to ease proofs. The Coq backend now generates Coq code compatible with Coq 8.8. A complete description of changes / new features can in found in the CHANGES file of the distribution. A complete description of changes / new features can in found in the CHANGES file of the distribution. The 0.9.2 release is available from focalize.inria.fr <http://focalize.inria.fr/> at http://focalize.inria.fr/download/focalize-0.9.2.tgz <http://focalize.inria.fr/download/focalize-0.9.2.tgz> Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.9.2 and follow the simple instructions written there. A public GIT repository is also available on GitHub (https://github.com/pessaux-f/focalize <https://github.com/pessaux-f/focalize>), allowing to fetch the latest development state of FoCaLiZe. However, its content is not bullet-proof and may be unstable at some times. It reflects the real-time state of FoCaLiZe and may bring fixes and features not available in previous releases and that will be part of the next release. To join people and discussions write to focalize-users@inria.fr <mailto:focalize-users@inria.fr>. Implementors also listen to suggestions (and compliments if some ^_^) at the mail address: focalize-devel@inria.fr <mailto:focalize-devel@inria.fr>. Enjoy. For the entire FoCaLiZe implementation group, François Pessaux. September 2018 What is it FoCaLiZe ? --------------------- FoCaLiZe is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLiZe provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of properties them from within the program source code. The FoCaLiZe compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator to produce Coq proof terms that are then formally verified. The FoCaLiZe compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developed in FoCaLiZe can be efficiently compiled to native code on a large variety of architectures. Last but not least, FoCaLiZe automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance. 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. FoCaLiZe is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantics, featuring a rock-solid infrastructure and greatly improved capabilities. -- 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 [-- Attachment #2: Type: text/html, Size: 7197 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [Caml-list] FoCaLiZe 0.9.2 released 2018-09-03 8:38 ` [Caml-list] FoCaLiZe 0.9.2 released François Pessaux @ 2018-09-03 16:02 ` David MENTRÉ 2018-09-03 17:06 ` Serge Le Huitouze 0 siblings, 1 reply; 3+ messages in thread From: David MENTRÉ @ 2018-09-03 16:02 UTC (permalink / raw) To: caml-list 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 ^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [Caml-list] FoCaLiZe 0.9.2 released 2018-09-03 16:02 ` David MENTRÉ @ 2018-09-03 17:06 ` Serge Le Huitouze 0 siblings, 0 replies; 3+ messages in thread From: Serge Le Huitouze @ 2018-09-03 17:06 UTC (permalink / raw) To: David MENTRÉ; +Cc: caml-list Hi all, I *don't* think it's inappropriate to answer to the list! --Serge On Mon, Sep 3, 2018 at 6:02 PM, David MENTRÉ <david.mentre@bentobako.org> wrote: > 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 -- 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 ^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2018-09-03 17:07 UTC | newest] Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <A04F917F-3FD5-42AD-BF41-61D2A4DC7A4A@ensta.fr> 2018-09-03 8:38 ` [Caml-list] FoCaLiZe 0.9.2 released François Pessaux 2018-09-03 16:02 ` David MENTRÉ 2018-09-03 17:06 ` Serge Le Huitouze
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).