Flying With Python (Strong versus Weak Typing)

[Alexander Schmolck]

Alex Martelli <aleax at aleax.it> writes:

> <posted & mailed>
> 
> Hasoob  ahs wrote:
> 
> > In an interview at http://www.artima.com/intv/strongweak4.html Guido
> > van Rossum was asked if "he would be comfortable enough with the
> > robustness of Python systems to fly on an airplane in which ALL the
> > control software was written in Python". Guido's answer was clear but
> > I would like to hear from other Python programmers.
> > Would you be comfortable?. Your answer may help me decide between
> > strong and weak typing. I prefer an answer of yes or no followed by an
> > explanation.
> 
> Yes!  The issue of what programming language[s] has/have been used in
> developing the control software is largely irrelevant to the issue of system
> safety, which depends instead on the process used for the development

This might be true in practice (I don't know much about what languages are
typically used for safety critical applications), but as an absolute statement
it seems rather dubious to me. The development process and language can't be
entirely seperable (e.g. how would you use a development process that stresses
formal proof with a language that has no formally specified semantics?). The
bugginess of the language itself would also seem to matter.

> If everything hasn't been *thoroughly* tested, AND programmed to be
> fail-safe to cover up for testing insufficiencies, the plane is not
> safe enough to use -- *whatever* language[s] it's programmed in --

It is simply not possible to thoroughly test something of reasonable
complexity, so I'd strongly prefer a language that allows interesting
(i.e. saftey-critical) properties of the system to be automatically verified
(e.g. range of output values, that no exceptions can occur in a certain
context, whatever). I am not sure to what extent this is currently possible.

I agree that mainstream statically typed languages like java don't seem to
offer that much of a reliability bonus (their type system mainly seems to
unearth realtively trivial errors that would have discovered by proper testing
anyway and its not clear that the code bloat it engenders doesn't introduce
possibly more severe errors and problems of its own).


> AND there must be fall-back safe systems that will further ensure against
> disaster if the impossible has occurred.

Fallback systems don't produce as much added safety as one might hope they
would, because even independently developed systems apparently have a large
overlap in their bugs.

 
> [Static typing] has no real bearing on safety issues for life-critical
> software.

I remember to have come across a few claims by rather smart people (like
Steele, who certainly is clued about dynamic languages, too) that the static
typing of ML languages can catch plenty of (nontrivial) errors. OTOH, I have
also heard of languages that have optional static type verification systems,
which however haven't turned out to be that useful in practice (Erlang,
possibly?). I haven't got any experiences myself -- have you?


alex