Formal specification and proof (was : Does Python really follow its philosophy of "Readability counts"?)

[James Mills]

On Thu, Jan 22, 2009 at 8:42 PM, Ricardo Aráoz <ricaraoz at gmail.com> wrote:
(...)

> What I've seen engineers do when they need extra safety is to put in place
> independently developed and operated redundant systems, at least three, and
> the system will do whatever two of the independent systems agree on. So I
> guess if I really wanted to be safe with a system I'd have it made by at
> least three different teams (yes, also the requirements should be written by
> different teams) in different languages under different OS's and different
> independent machines. And THEN I would have some measure of safety (and this
> would certainly be more cost effective than the formal specification route).

This is quite honestly the best thing I've seen
written on this very topic of safety and mission
critical systems! Thank you!

My entire point(s) throughout this very long and tediously
boring thread have been that one language over another
doesn't necessarily bear much weight on the safety
requirements of a system.

One thing that those that have argued for Data Protection,
Static Typing, Strong Typing and Stricter Encapsulation (all of
which Python -IS NOT- and -WILL NOT- be); is that Safety
Requirements are normally intangible, unquantifable
measures. How do you rate the safety of your system ? By
the number of deaths and injuries it not cause ? By the fact
that your Shuttle doesn't blow up ? Your plane landing correctly ?

Ricardo's point is very well put and Safety Critical systems
that specify requirements, tangible and quantifiable requirements
are what makes a system safe and gives assurance - not the language
or the platform os the os or the environment. For example:

FR1: When the landing gears button is pressed, the landing gears will
be lowered and monitored and confirms by the Confirmation System and
Verified by the Verification System.

Have a pleasant day,

cheers
James