This can be of interest to many of you still bound to C++. This
language is aimed as a "better C++", it compiles (translates) to C++,
and has many features from modern languages esp. from the ML family
and from Haskell (while still keeping the good things of C++, as far
as I can tell).
---------- Forwarded message ----------
From: skaller <[EMAIL PROTECTED]>
Date: May 12, 2007 7:06 AM
Subject: [Caml-list] Felix 1.1.3 released
To: [EMAIL PROTECTED]
Felix 1.1.3 has been released and can be obtained from
http://felix.sourceforge.net/flx_1.1.3_rc4_src.tgz
(it's release candidate 4, but that's final in the 1.1.3).
It should build on all Unix systems, OSX, Cygwin, Win32,
and Win64 (using VS2005=VC7 or VS2007=VC8 compilers).
You will need Python, Ocaml, and either g++ or MSVC++ installed.
Please join mailing list for help building on Windows platforms.
Felix is an advanced language in the Algol/ML family,
with technology and ideas stolen from Ocaml and Haskell.
It generates ISO C++ code, and provides facilities for
easy binding to C and C++ using a NFI (Native interface)
generally not requiring any external glue logic.
It also features high performance user space cooperative
threading.
Licence: FFAU (roughly BSD).
Roughly it is designed for C++ programmers who can't afford
to throw out legacy C/C++ libraries or frameworks,
Ocaml/ML/Haskell programmers with the same problem,
applications requiring very high performance,
or researchers who want to implement production variants
of research ideas in a open code base.
This release was a long time coming because it adds a major
new feature -- Haskell style typeclasses. This facility
is equivalent to C++ template specialisation, but done right.
Second order support is 'just enough' to provide a Monad
typeclass.
In addition, this release supports first order axioms, reductions,
and lemmas. Reductions are user defined term rewriting rules.
Lemmas are propositions which can be proven from axioms.
These assertions can be written in typeclasses to provide
formal specification of some semantics.
Apart from automated checking of axioms by use cases, Felix now
emits Why code representing the axioms, and makes any
lemmas goals. The generated files can be submitted to
a theorem prover via Jean-Christophe Filliâtre Why program
http://why.lri.fr/
or directly to Ergo. This system is of course work in
progress, but it does verify at least one simple lemma :)
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-----
This list is sponsored by AGIRI: http://www.agiri.org/email
To unsubscribe or change your options, please go to:
http://v2.listbox.com/member/?member_id=231415&user_secret=fabd7936
