Rust is better than Haskell for everything, even for provers. Here is why
Feel free to post this text somewhere, say, in your blog
A lot of points below matter for provers
- Rust has bigger community than Haskell and more packages in standard packages repository
- Rust is imperative and this is good thing. Even code for generating proof objects benefit from ability of doing imperative things. For example, this is PhD dissertation, where author developed his new programming VeriML for dealing with formal proofs: https://astampoulis.github.io/veriml/dissertation.pdf . His language is imperative, and author considers this as a feature, he writes how imperative features help him to deal with proof objects
-- When I need to write imperative code in Haskell (and I really need this sometimes) I had to resort to ST monad. And the result looks ugly. For example, here is my code: https://hackage.haskell.org/package/check-cfg-ambiguity-0.0.0.1/docs/src/CheckCFGAmbiguity.html#lowLevelTestAmbiguity (this code checks whether given context free grammar is ambiguous). Find "runST" in the code and look how ugly the code is! Equivalent code in imperative Rust looks better
-- Haskell is pure language, and this makes it slow, for example, when you need to update arrays. Well, in fact Haskell *does* provide you way to update arrays *safe* and *fast* simultaneously: using linear haskell. But Rust is linear, too! (Well, edit: affine). And Rust's syntax for affine updating arrays is way easier to use than haskell's! Moreover, despite haskell has linear types, it still has nothing like Rust's Vec::push. I. e. you cannot imperatively lineary push new value to a vector in haskell. But in rust you can
- Rust has a way better tooling. No cabal/stack dichotomy. Cargo.toml is usually shorted than gigantic *.cabal file. No "cabal v1-install" vs "cabal v2-install" insanity. No multiple different unit testing frameworks. One true unit testing framework built into language. Doctests built into language, too. No "doctests.hs" hacks
- Rust is free of historical baggage. No "String" vs "Text" insanity
- Rust is faster than Haskell (and I don't need garbage collector anyway). I rewrote above mentioned CheckCFGAmbiguity.hs in Rust and the resulting code is 13x faster (i didn't spend time manually optimizing both versions). And the rust code is free of ugly ST monad
- Some people say that haskell is somehow "formal math". But it is not. Currently haskell doesn't contain built-in prover. I. e. you still cannot write "head", which takes proof object, proving that the list is non-empty. And even when dependent haskell arrives, it still will not contain prover, because there is no plans to add termination checker in dependent haskell. So, there is no any point in waiting for depending haskell. If you need formal math, use languages, which *really* contain provers, such as Agda. In other words, there is no room for haskell. If you need formal math, use Agda (or Coq). For everything else use Rust. That is
- Rust is safer. Because compiler errors when you missed some data constructor in "switch" statement. GHC by default don't give you even a warning. Yes, this matters. Yes, it is easy to forget to add needed flag for ghc
- Yes, haskell has richer type system. But I never actually needed it. Except in cases where this rich type system is used to workaround lack of imperative features (i. e. haskell lenses are needed, because we cannot do usual record update)
-- Please, note: I understand why pure languages exist. I simply want to say that I always feel programming imperative languages a way easier than pure ones. Even for prover, because even in them we need imperative mutable data structures in big practical programs
- In provers you often want to compare terms for equality. And often such terms happens to be same term, so recursive compare is not practical. So, you need pointer equality (and then resorting to recursive compare if pointers happen to be not equal). Unfortunately, in haskell function for pointer equality named "reallyUnsafePtrEquality#". I. e. it is as dangerous-looking as it possibly can be. Not only its name contain word "unsafe", it is even "really unsafe". And finally we have "#" in the end. Aaaah. This is hands up for anyone doing code review. In Rust you do normal pointer equality, and the code doesn't look dangerous at all
- In the past I used haskell for provers and c++ for everything else (usually system programming tasks, such as "write my own coreutils"). But now rust can replace both languages! It is "one language to rule them all"! I *can* do system programming tasks in it. And I can write provers. Cool!
Please, note: some of this arguments are not convincing if used alone. For example, argument "haskell doesn't contain prover", of course, is not convincing, because rust doesn't contain prover, too. But this argument works if used in combination with others. Haskell doesn't contain prover, rust doesn't, too. But rust has greater tooling. See? :)