PEP 3107 and stronger typing (note: probably a newbie question)

[Bruno Desthuilliers]

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 ?-)