Hello David, Thus quoth David McClain at 15:39 on Tue, Apr 18 2017:
1. Machine Fault failures on successfully compiled code. That’s the big nasty one. Provably correct code can’t fail, right? But it sometimes does.
A very small remark (mostly directed at novice Haskell users reading this): code which typechecks is _not_ the same thing as _provably correct_ code. Code which typechecks is code in which function applications concord with the types. Provably correct code is code which was (or can be) (automatically) proved to correspond to a certain exact specification. Haskell or OCaml type systems are usually not used for writing such exact specifications, because they are not expressive enough. Thus, in general, showing that Haskell or OCaml code typechecks is weaker than proving that it has a certain property (like not failing). (However, passing Haskell or OCaml type checks is still stronger than passing Java type checks.)
And I think you can trace that to the need to interface with the real world.
I have the same gut feeling. -- Sergiu