[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