[Python-ideas] Pre-conditions and post-conditions

[Steven D'Aprano]

On Wed, Aug 29, 2018 at 02:26:54PM +0100, Jonathan Fine wrote:

> This is about a difference of opinion regarding design by contract and
> static checking, that Steve D'Aprano has re-raised. Steve wrote that
> Ivan Levkivskyi's opinion was that:
> 
> > contracts [are] always statically checked
> 
> This is what Ivan wrote:
> 
> > TBH, I think one of the main points of design by contract is that contracts
> > are verified statically.
> 
> There's no 'always' or 'all' here. I read it to mean 'sometimes' or
> 'some'. And also, that static verification is a good thing.

Fair enough, I should not have added "always" in my description.

But you probably shouldn't have skipped the part I wrote earlier:

"Contracts may be verified statically if the compiler is able to do so, 
but they are considered runtime checks. Static checks are an 
optimization."

In context, you quoted me disagreeing with the "static" claim, but 
trimmed out my qualification that contracts may sometimes be statically 
verified when possible.


[...]
> > Ivan said that static checking was a main point. Those Eiffel docs which
> > you (Jonathon) quoted approvingly describe them as "run-time
> > assertions".
> 
> I'm sorry, but I'm just not seeing that. Either in what I quoted, or
> elsewhere in the page. True, my quote is from a section titled
> "Run-time assertion monitoring", but the context to me makes it clear
> that in Eiffel static typing IS NOT regarded as a run-time assertion.

Of course it isn't. By definition, static typing is done *statically*, 
at compile-time, not run-time. That has not been questioned and nobody 
has asserted that static typing is done at run-time.

We're discussing whether *contracts* are checked at run-time.

Because contracts are (in general) run-time assertions, they are a good 
fit for Python's execution model -- or at least they would be if we can 
find a good way to apply contracts to methods and classes. If they were 
static, they would be a bad fit and would probably need to be handled by 
a separate static checker, like MyPy does for static type checks.



-- 
Steve