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

[Diez B. Roggisch]

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