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 <[EMAIL PROTECTED]> 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
