> > wrt/ proofs of correctness, I'll just point to the spectacular failure > of Ariane, which was caused by a *runtime* type error in a system > programmed in ADA - one of the languages with the most psychorigid > declarative static type systems.
That's simply not true. The problem hadn't to do with typing - it was a overflow due to larger input quantities. It had been shown for the Ariane 4 that this overrun could never happen - by whatever thechnique, operational or denotational semanticse, I don't know. For the ariane 5, these input constraints didn't hold, which caused the unexpected runtime error to occur. But there is _no_ type-error here! The programmers might have chosen a different type with larger range, sure. But to say that's a type error is as saying "using a string where a tuple of int and string were better is a type error." It's another path of implementation. Or from a testing angle: if the unit tests did only produce input values to a certain quantity, the results were ok. Nobody thought about writing new tests with larger quantities - the same way nobody thought about proving the program with those same quantities. Diez -- http://mail.python.org/mailman/listinfo/python-list
