[Haskell-cafe] Optimization with Strings ?

Don Stewart dons at galois.com
Thu Dec 3 11:39:46 EST 2009


JohnDEarle:
> You may want to look into Objective CAML http://caml.inria.fr/ which is a
> French product as you can see from the Internet address. It is likely better
> suited to the task than Haskell and has a reputation for speed. For those who
> prefer object oriented programming it has facilities for that which may ease
> your transition from C++. The Microsoft F# language is based on Objective CAML.
>  
> Haskell has a problem with its type system and is not rigorous. Haskell is not
> a suitable language for proof assistants and so I would advise you to stay
> clear of Haskell. Standard ML was engineered with the needs of proof assistants
> in mind and so you may want to look into Standard ML, but you should be very
> happy with Objective CAML. It has an excellent reputation. The Coq proof
> assistant which is another French product is based on Objective CAML.

Ok, that is serious trolling. There are several proof assistants written
in Haskell:

    http://hackage.haskell.org/package/Agda
    http://hackage.haskell.org/package/ivor
    http://www.e-pig.org/
    http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila
    http://www.cwi.nl/~jve/demo/
    http://www.haskell.org/dumatel/
    http://www.cs.chalmers.se/~koen/folkung/
    http://taz.cs.wcupa.edu/~dmead/code/prover/ 
    http://www.math.chalmers.se/~koen/paradox/
    http://proofgeneral.inf.ed.ac.uk/Kit
    http://www.haskell.org/yarrow/

and the guarantees of purity the type system provides are extremely
useful for verification purposes. 

Please, before posting like this to the Haskell community, inform
yourself more of what the Haskell community has produced.

-- Don


More information about the Haskell-Cafe mailing list