Live data from Hacker News

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

news.ycombinator.com

11–14 of 14 posts

Re: Ask HN: A well-typed program won't go wrong?

#12

> I've read a few times here on HN the saying > "a well-typed program won't go wrong" or some > slight variation. Actually, I don't remember seeing that stated here on HN. Could you provide some references? I don't know anyone who says that. Seriously strict typing can prevent certain types of errors, and can ensure that the code runs. But if I implement quicksort when I intended to implement heapsort, how can typing…

There are a few people discussing or mentioning the phrase, but I didn't find anyone actually making the claim.

https://www.google.com/search?q=a+well-typed+program+won't+g...

Re: Ask HN: A well-typed program won't go wrong?

#13
post #10

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 rand…

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.

Re: Ask HN: A well-typed program won't go wrong?

#14
post #10

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 rand…

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 pe…

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.
Post reply on HN