That's a very nice point. However precision comes at a cost, usually in verbosity and understandability. Coq, for example, requires even more precision. It's g

That's a very nice point. However precision comes at a cost, usually in verbosity and understandability. Coq, for example, requires even more precision. It's great for math, but terrible for writing a database. For the systems I wanted to build, even Haskell feels needlessly precise in the areas I tend to get right in short order, but there's no (or not enough) support in the cases where I could use some help, such as the behavior of an O/S or database or network. I prefer F# and Erlang in their balance between precision, safety and system building ability.