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

[Paul Rubin]

James Mills <prologic at shortcircuit.net.au> writes:
> 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. 

But it is characteristics of the language, platform os, and
environment, that make it easier or more difficult to provide high
assurance that the specifications are actually met.  See this article
for the meaning of "high assurance":

   http://www.dwheeler.com/essays/high-assurance-floss.html 

Basically, high assurance in the view of the folks who issue
specifications for it and fund it, requires a lot of static
verification.