Static typing, Python, D, DbC

[Eric S. Johansson]

  On 9/12/2010 4:28 PM, Paul Rubin wrote:
> Bearophile<bearophileHUGS at lycos.com>  writes:
>> I see DbC for Python as a way to avoid or fix some of the bugs of the
>> program, and not to perform proof of correctness of the code. Even if
>> you can't be certain, you are able reduce the probabilities of some
>> bugs to happen.
> I think DbC as envisioned by the Eiffel guy who coined (and trademarked)
> the term is that it's a static verification technique, marketing-speak
> annotating subroutines with pre- and post- conditions that can be
> checked with Hoare logic.  Runtime checks wouldn't qualify as that.
Programming by contract as popularized by Bertrand Meyer (that Eiffel guy) was 
designed for run-time checks because that's when errors show. Programming by 
contract is based on Dijkstra's weakest precondition work.  
http://www.scss.tcd.ie/Edsko.de.Vries/talks/weakest_precondition.pdf

During the last five years before my hands went bad, I spent  significant amount 
of time working with formal methods  and simpler concepts such as design by 
contract. Design by contract made the last five years of my programming career 
the most rewarding it had ever been. It was nice to finally write code that was 
significantly, and measurably better than those coded using Brown 25  (another 
fine product from Uranus)[1].

one of the common mistakes have seen about programming by contract or design by 
contract is that people assume it's a proof of correctness. It's not, it's an 
experiential proof that the code is executing correctly to the extent that 
you've characterized the pre-and post-conditions. Formal proofs are considered a 
dead-end as far as I can tell but it's been a good number of years since I've 
really investigated that particular domain.

If my opinion is worth anything to anyone, I would highly recommend adopting 
some form of programming by contract in everything you write.  use the 
properties that Dijkstra taught us with the weakest precondition to test only 
what you need to test. If you are careless, assertions can build up to a 
significant percentage of the code base and Slow execution. the argument for 
dealing with this, last time I looked, was that you turn off assertions when 
your code is "running". This logic is flawed because bugs exist and will assert 
themselves at the worst possible time which usually means after you turned off 
the assertions. Personally, I see assertions as another form of defensive 
programming. If you can define preconditions as excluding bad data, then your 
mainline body becomes faster/smaller.

Anyway, this debate was going on circa 1990 and possibly even earlier when 
Dykstra wrote his first papers. Consider me a double plus vote for strong 
programming by contract capability in Python. If I can ever get programming by 
voice working in a reasonable way, I might even be able to use it. :-)

PS, to explain Brown 25 in case you weren't watching "those damn kids" comedy 
movies in the 1970s with a bunch of very stoned friends.  Thank God for campus 
buses keeping us out of cars.
[1] http://www.youtube.com/watch?v=008BPUdQ1XA