Does Python really follow its philosophy of "Readability counts"?

[Paul Rubin]

"Russ P." <Russ.Paielli at gmail.com> writes:
> I don't know which variant of Ada was used here, but something called
> the "Ravenscar Profile" is a reduced subset of Ada that might have
> prevented this error (though I haven't verified this). Then there is
> Spark Ada, which supposed to be much safer than even Ada.

I'm not sure, but I think Ravenscar and Spark would both have
permitted the cast.  However, Spark is intended to be used with an
external tool called Spade (sort of a Pylint on steroids) that would
not have allowed the cast unless it was provable (starting from the
specification) that the number was in range before the cast.

I.e. the cast was wrong because of the failure of an unstated
assumption that a certain sensor reading was in a certain range.
Spark may still have allowed the cast only if the assumption was
stated explicitly in the specification.  Requiring the assumption to
be stated may have made the error more likely to be spotted as part of
the surrounding systems engineering.  Of course, the specification can
still be wrong, but that's hardly a problem with Ada or even with the
software.  It's not too much different than if the specification says
the rocket is 10 feet wide and they build the launch pad for that
size, but then the rocket turns out to actually be 12 feet wide.

I have Barnes's book about Spark at the office and will try to check
next week what it says about these casts.