Static typing, Python, D, DbC
Static typing, Python, D, DbC The Python computer language
I write some Python code almost every day, but lately, I am using a lot the D language too. After using D for about three years I now know some of it, but when I need to write short (< about 1000 lines) *correct* programs, Python is still the more productive for me. Static typing and the usage of transitive const of D are a strange thing. It seems obvious that they lead to safer code, but on the other hand, experimentally I have seen that my short Python programs are less buggy than equivalent D ones. Static typing looks safer, but D offers many low-level features, and generally, it contains many more traps or ways to shoot your own foot, that they more than compensate for the “lack of safety” coming from Python dynamic typing, even when you don’t use those low-level features. Maybe for large (> about 100_000 lines) programs D may come out to be less bug-prone than Python (thanks to the better data hiding and static typing), but I am not sure of this at all… Static typing also has a significant cost. When you write D2 code often something doesn’t work because of some transitive const or immutable (or just because of the large number of bugs that need to be fixed still in the D compiler). So here you pay some cost as debugging time (or time to avoid those problems). And there is a mental cost too because you need to keep part of your attention on that const- related things instead of your algorithms, etc. — — — — — — — — Lately while I program with Python one of the D features that I most miss is a built-in Design By Contract (see PEP 316) because it avoids (or helps me to quickly find and fix) many bugs. In my opinion, DbC is also very good used with doctests. You may implement a poor’s man DbC in Python like this: class Foo: def _invariant(self): assert … assert … return True def bar(self, …): assert self._invariant() … res = … assert self._invariant() return res But this missed several useful features of DbC. split (something like a str.xplit()). In some situations, it reduces memory waste and increases code performance.
I would do it like this: from DbC import DbC class Foo(__metaclass__=DbC): def __invariant(self): … automatically asserted for all methods … def __precond(self): … automatically asserted for all methods … def __postcond(self): … automatically asserted for all methods … @precond(attr=value) # asserts self.attr==value @postcond(func) # a function for more complex assertions def bar(self, …): … clean, uncluttered code … and set DbC.uninstall() to uninstall all precond/postcond/invariants at runtime without any additional overhead. These are all definitely possible with metaclasses and decorators. Care to open an issue at the tracker? Considering that many Python 3 builtins are now lazy, there might be a chance this is an oversight, or there might be a reason why string. split is not lazy.
Design by contract really isn’t a good fit for Python. I’ve done proof of correctness work, and there are suitable languages for it. It needs a language where global static analysis is possible, so you can reliably tell what can changes what. John Nagle
John Nagle: I have used some times the class invariant done manually, as I have shown, and it has avoided me some bugs, so I have experimentally seen you are wrong. 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 to 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 a significant amount of time working with formal methods and simpler concepts such as design by contract. Design by the 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 signed, 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.
