First release of focalize, a development environment for high integrity programs.

First release of focalize, a development environment for high integrity programs.

[Pierre Weis]

Hi to all of you careful bug hunters and happy hackers reading this message!

It is my pleasure to announce the first public release for FoCaLize, a purely
functional language and environment to express and formally prove algorithms
and their implementation.

(0) What is it ?
----------------

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 those properties 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 that produces in turn the Coq
proof terms that are formally verified.

The FoCaLize compiler also generates the code corresponding to the
program as an Objective Caml source file. This way, programs developped 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 such an 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 done 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.

(1) Where to find it ?
----------------------
FoCaLize home page is http://FoCaLize.inria.fr/
FoCaLize source files can be found at
http://FoCaLize.inria.fr/download/focalize-0.1.0.tgz

(2) How to install it ?
-----------------------
Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.1.0 and follow the simple instructions written there.


Enjoy.

For the entire FoCaLize implementor group,

Pierre Weis.

Tuesday, March 24, 2009 10:05:13

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[David MENTRE]

Hello,

Thank you for the announcement. The project seems quite interesting.

On Tue, Mar 24, 2009 at 11:07, Pierre Weis <weis@deby.inria.fr> wrote:
> (1) Where to find it ?
> ----------------------
> FoCaLize home page is http://FoCaLize.inria.fr/
> FoCaLize source files can be found at
> http://FoCaLize.inria.fr/download/focalize-0.1.0.tgz

For those interested in such details, FoCaLize seems to be under a
BSD-like license (I have not made a detailed review of the code). I
would be interested to know if knowledged people (e.g. Debian
developers ;-) consider this code Free Software or not.

====LICENSE====
  Copyright (c) 2007-2009, Institut National de Recherche en
  Informatique et en Automatique (INRIA), LIP6 (Laboratoire d'Informatique de
  Paris 6)

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

  * Redistributions of source code must retain the above copyright notice,
    this list of conditions and the following disclaimer.

  * Redistributions in binary form must reproduce the above copyright
    notice, this list of conditions and the following disclaimer in the
    documentation and/or other materials provided with the
    distribution.

  * Neither the name of INRIA nor the names of its contributors may
    be used to endorse or promote products derived from this software
    without specific prior written permission.
[...]
====

Sincerely yours,
david

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Martin Jambon]

David MENTRE wrote:
> For those interested in such details, FoCaLize seems to be under a
> BSD-like license (I have not made a detailed review of the code). I
> would be interested to know if knowledged people (e.g. Debian
> developers ;-) consider this code Free Software or not.

Let me take the bait and bury it.
Such discussion would be 100% off-topic.


Thanks.

Martin

-- 
http://mjambon.com/

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Erik de Castro Lopo]

David MENTRE wrote:

> For those interested in such details, FoCaLize seems to be under a
> BSD-like license (I have not made a detailed review of the code). I
> would be interested to know if knowledged people (e.g. Debian
> developers ;-) consider this code Free Software or not.

I am not a Debian Developer, but this seems to be what the Free
Software Foundation calls a modified BSD license:

    http://www.xfree86.org/3.3.6/COPYRIGHT2.html#5

This is just one of the licenses that the FSF considers a GPL
compatible license:

    http://www.gnu.org/philosophy/license-list.html

As a GPL compatible license, I think most people, including
DDs would consider this Free Software.

Erik
-- 
----------------------------------------------------------------------
Erik de Castro Lopo
http://www.mega-nerd.com/

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[David MENTRE]

Hello Martin,

On Tue, Mar 24, 2009 at 12:08, Martin Jambon <martin.jambon@ens-lyon.org> wrote:
> David MENTRE wrote:
>> For those interested in such details, FoCaLize seems to be under a
>> BSD-like license (I have not made a detailed review of the code). I
>> would be interested to know if knowledged people (e.g. Debian
>> developers ;-) consider this code Free Software or not.
>
> Let me take the bait and bury it.
> Such discussion would be 100% off-topic.

I'm sorry to strongly disagree. I consider part of an annoucement to
know the *precise* license under which a software is released (free
software or not).

A working or personnal environment can preclude the use of softwares
under certain licenses.

Many thanks to Erik for his constructive reply (which I should have
done myself).

Sincerely yours,
david

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Stefano Zacchiroli]

On Tue, Mar 24, 2009 at 11:55:52AM +0100, David MENTRE wrote:
> For those interested in such details, FoCaLize seems to be under a
> BSD-like license (I have not made a detailed review of the code). I
> would be interested to know if knowledged people (e.g. Debian
> developers ;-) consider this code Free Software or not.

I certainly would. [*]

Actually, the license snippet you posted matches what is shipped on
Debian machines as /usr/share/common-licenses/BSD , a license under
which hundreds of Debian-packaged softwares are currently released.

Cheers.

[*] FWIW, I'm replying only accordingly to your mail and I haven't
    checked all of focalize's source files.

-- 
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Dietro un grande uomo c'è ..|  .  |. Et ne m'en veux pas si je te tutoie
sempre uno zaino ...........| ..: |.... Je dis tu à tous ceux que j'aime

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Richard Jones]

On Tue, Mar 24, 2009 at 11:07:29AM +0100, Pierre Weis wrote:
> (0) What is it ?
> ----------------
> 
> 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 those properties from within the program source code.

Are there any examples / tutorials?  I skimmed the reference manual
and it has to be said I found it fairly baffling.

Rich.

-- 
Richard Jones
Red Hat

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Raoul Duke]

> Are there any examples / tutorials?  I skimmed the reference manual
> and it has to be said I found it fairly baffling.

furthermore (i /am/ trying to get time to read the docs on the site
:-), how does it compare to other things which i /ass/ume are in a
similar 'space' e.g. SPARKAda etc. thanks!

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[Damien Doligez]

On 2009-03-24, at 11:55, David MENTRE wrote:

> For those interested in such details, FoCaLize seems to be under a
> BSD-like license (I have not made a detailed review of the code). I
> would be interested to know if knowledged people (e.g. Debian
> developers ;-) consider this code Free Software or not.


In my (off-topic for this list) opinion, this whole licence business
is totally out of control because lawyers have succeeded in scaring
everyone witless about it.  For example, I don't understand why you
would need a detailed review of the code in order to notice that the
licence (which you quoted) is an exact copy of the new BSD licence
(straight from www.opensource.org, IIRC).

Whether you (or the Debian developers, Microsoft management, or
whoever else) choose to call it Free is a matter of political
opinion and debate on this topic is usually a waste of time.

This was my license rant for 2009.  Thanks for your attention.

-- Damien

Re: [Caml-list] First release of focalize, a development environment for high integrity programs.

[David MENTRE]

Hello,

On Wed, Mar 25, 2009 at 10:02, Damien Doligez <damien.doligez@inria.fr> wrote:
> For example, I don't understand why you
> would need a detailed review of the code in order to notice that the
> licence (which you quoted) is an exact copy of the new BSD licence
> (straight from www.opensource.org, IIRC).

I already acknowledged that I should have noticed that the license is
an exact copy of the new BSD license. However, from past experience,
it happens that such software coming from a national or european
project with multiple contributors might mix multiple (and even
incompatible) licenses for the different part of the code. Thus my
question regarding code review. (I'm *not* saying this is the case for
Focalize)

> Whether you (or the Debian developers, Microsoft management, or
> whoever else) choose to call it Free is a matter of political
> opinion and debate on this topic is usually a waste of time.

I entirely agree (for caml-list@). I'll should have avoided this part
of the question.

<formal tools rant for 2009>
Formal verification tools have such a high cost to learn and use them
that I personally won't *consider* them if they not Free Software
(according to FSF or Debian). It is hard enough to convince colleagues
and management of the usefulness of such tools without being annoyed
by restriction of use.
</rant>

Yours,
d.