[Haskell-cafe] Wow Monads!

[Sergiu Ivanov]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170418/69e641f3/attachment.sig>