Am 18.04.2017 um 23:33 schrieb Sergiu Ivanov:
Haskell or OCaml type systems are usually not used for writing such exact specifications, because they are not expressive enough.
I have read statements that Haskell code still tends to "just work as expected and intended", and see that attributed to the type system. Seemed to be related to Haskells expressivity, with the type system pretty much preventing the typical errors that people make. So the sentiment was that it's not the same but close enough to be the same in practice. Though I doubt that that will hold up once you get more proficient in Haskell and start tackling really complicated things - but "simple stuff in Haskell" tends to get you farther than anybody would expect, so it's still a net win. Just impressions though, I never had an opportunity to delve that deeply into Haskell.
Thus, in general, showing that Haskell or OCaml code typechecks is weaker than proving that it has a certain property (like not failing).
That a code type checks in Haskell still gives you a whole lot of guarantees. Such as "it doesn't have IO in the type signature so there cannot be any side effect deep inside". (Ironically, people instantly started investigating ways to work around that. Still, the sort-of globals you can introduce via the State monad are still better-controlled than the globals in any other language.) (Aside note: I don't know enough about OCaml to talk about its properties, but I do believe that they are much weaker than in Haskell.)
(However, passing Haskell or OCaml type checks is still stronger than passing Java type checks.)
Yep.
And I think you can trace that to the need to interface with the real world.
I have the same gut feeling.
I think interfacing with the outside world (still not "real" but just bits inside the operating system and on disk) is one major source of unreliability, but not the only one, and not necessarily the primary one. YMMV.