Software bugs aren't inevitable

A work colleague circulated this interesting article about reducing
software bugs by orders of magnitude:
http://www.spectrum.ieee.org/WEBONLY/publicfeature/sep05/0905ext.html

Some methods they talk about include removing error prone and ambiguous
expressions from their ADA based language Sparc - The example they give
is on why they removed the increment operators x++, x-- .

A bit of googling shows that they have, in the past mentioned Python in
Job specs, but only as one of many languages.

I was wondering what Praxis thought of Python, and how good it would be
if a Praxis engineer gave a critique of Python as a part of a flow for
producing low bug-count software.

In this sidebar to the main article:

http://www.spectrum.ieee.org/WEBONLY/publicfeature/sep05/0905extsb1.html

It seems that they use one equation from the Z notation model and add
it as a comment to their main programming languages function definition
as a comment, then have a means of automatically testing the comment
against the function body.

This is rather like how doctest can check the test and expected result
given in a doc-string against the implementation given in the function;
indeed I wrote up such an example at work and circulated it amongst the
resident perl mongers. - Gosh it fealt good :-)

So, How do I get feedback from Praxis, Do they already read
comp.lang.py?

Cheers, Paddy.

.