“Well-typed programs don't go wrong.” This slogan for ML-style static typing is infamous, since it's true only under an extraordinarily narrow definition of “go wrong”. This definition is not used for any other purpose, so it's virtually impossible for an innocent listener to arrive at the “correct” interpretation. For propaganda purposes, this is a feature, as it allows the user to make an outrageous claim and then blame its falsity on the audience's ignorance.
The slogan is a little bit justifiable in its original context. Robin Milner introduced it (along with polymorphic type inference) in his 1978 paper A Theory of Type Polymorphism in Programming, as the heading “Well-Typed Expressions Do Not Go Wrong”. The original use refers to a toy language in which the only possible runtime errors are type errors, so the typechecker really does prove the absence of all errors. Well-typed expressions, in that language, can loop forever or run out of memory, but they can't have semantic errors: they can't “go wrong”.
Milner must have known it was misleading, though.
Does that make April 19, 1978 a day that will live in infamy?
ReplyDeleteInfamy? It's more of a “shot heard round the world”. This is the paper that introduced practical type inference, and anticipated extensions to autoconversion and overloading, and spawned a language family and a subfield. Unlike many later papers in that subfield, it clearly distinguishes theory from practice, and (pet peeve alert!) doesn't present a useful tool as an essential semantic foundation. For these virtues, a misleading slogan can be forgiven.
ReplyDelete