Diez B. Roggisch a écrit : >> >> 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.
cf below. > 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. IIRC it was in the specs. > For the ariane 5, these input constraints didn't hold, which caused the > unexpected runtime error to occur. """ Because of the different flight path, a data conversion from a 64-bit floating point to 16-bit signed integer value caused a hardware exception (more specifically, an arithmetic overflow, as the floating point number had a value too large to be represented by a 16-bit signed integer). """ As far as I'm concerned, it surely qualifies as a runtime type error - "data conversion from a floating point to a 16-bit signed int" should not be allowed when unsafe, isn't it ? """ Efficiency considerations had led to the disabling of the software handler (in Ada code) for this error trap. """ Which implies that even in ADA, runtime type errors are in fact expected - else there would be no handler for such a case. The root of the problem is - of course - not technical but human. As you said, no one cared to write the appropriate unit tests to ensure this module - specified for Ariane 4 - could be reused 'as is' for Ariane 5. But what, how could an ADA module not be correct if it compiles - the ADA type system is here to "prove the absence of certain bugs", isn't it ?-) -- http://mail.python.org/mailman/listinfo/python-list
