[Haskell-cafe] ANN: The Disciplined Disciple Compiler - alpha 1.1

[Robin Green]

Is there any work on combining effect typing with extended static
checking or full-blown formal verification (e.g. proof-carrying code)?
My hunch would be that an impure functional language like this (OCaml is
another example) makes optimisation easier, compared to Haskell - but at
the expense of making formal reasoning about the code potentially as
complicated and hard as formal reasoning about, say, Java code.

Of course, the way in which programmers choose to use the language
would impact how easy their code is to reason about. But from the
standpoint of ease of reasoning, I'm leaning towards sticking with pure
languages for the time being, in my research.
-- 
Robin

On Thu, 3 Jul 2008 22:12:30 +1000
Ben Lippmeier <Ben.Lippmeier at anu.edu.au> wrote:

> 
> Hi All,
> I'm pleased to announce version 1.1
>     of the Disciplined Disciple Compiler (DDC)
> 
> Disciple is an explicitly lazy dialect of Haskell which supports:
>   - first class destructive update of arbitrary data.
>   - computational effects without the need for state monads.
>   - type directed field projections.
>   - allied functional goodness.
> 
> All this and more through the magic of effect typing.
> 
> New in this version:
>   - support for x86_64 under linux and darwin, thanks to Jared Putnam.
>   - the -make flag now does a full dependency driven build/rebuild.
>   - constructor classes.
>   - irrefutable patterns.
>   - partial support for monadic do notation.
>   - an unboxed Bool# type with true# and false# literals.
>   - field projection punning.
>   - lots more example code.
> 
> Project page with full release notes and download at:
>    http://www.haskell.org/haskellwiki/DDC
> 
> DDC: more than lambdas.
> 
> Ben.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>