[Haskell-cafe] Wow Monads!
sivanov at colimite.fr
Tue Apr 18 21:33:48 UTC 2017
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
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
> And I think you can trace that to the need to interface with the real
I have the same gut feeling.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 487 bytes
Desc: not available
More information about the Haskell-Cafe