News for hackers. Stuff that matters.

A comment on Ask HN: A well-typed program won't go wrong?.

Re:Ask HN: A well-typed program won't go wrong? by tome on Monday November 03, 2014 @05:25PM (#8553963)
OK, let's knock this on the head very quickly please and avoid a flamefest.

According to "Generalized Arrows"[1] by Adam Megacz Joseph the slogan "Well typed programs do not go wrong" was coined by type theorist Robin Milner and means something very specific: 'To "go wrong" means to exhibit undefined behavior. For example, programs written in strongly statically typed programming languages cannot crash, write to random memory locations, or read past the end of a buffer.' If you want precise details please read Milner's "A Theory of Type Polymorphism in Programming"[2].

Note that this does not imply that well typed functional programs do not contain bugs. Futhermore it only applies to a very specific ML-like language with a precisely defined denotational semantics. It is not known to apply to Haskell as no one has even written down the denotational semantics for Haskell. Furthermore it is trivially easy to write crashing programs in most Haskell implementations by taking advantage of any of a variety of non-standard features and functions.

Please let us not build up and knock down straw men about Haskell claiming to prevent all bugs.

[1] http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-13...

[2] http://tfeng.me/papers/milner78theory.pdf

[ Parent | on HN ]
Re:Ask HN: A well-typed program won't go wrong? by AnimalMuppet on Monday November 03, 2014 @06:51PM (#8554341)
Then does ML's type system detect my "+ 1" error? Or does ML not crash once memory is exhausted? Or does "crash" in your second paragraph really mean "crash due to reading an invalid memory location"? (I'm not trying to be argumentative here; I'm trying to understand. I don't understand ML well enough to answer my questions.)

I accept Milner's claim, with his definition of "go wrong". The problem then becomes that people repeat the claim, but not the definition, and so people like me hear the claim, don't know the technical definition of "go wrong", and assume that the general meaning of the words is being used.

[ Parent | on HN ]
Re:Ask HN: A well-typed program won't go wrong? by tome on Tuesday November 04, 2014 @06:22AM (#8556012)
If people are saying "well typed programs don't go wrong" to mean something other than the precise technical statement then you or I will have to correct them. However you will have to point me to some examples first. I couldn't find any.
[ Parent | on HN ]