status of Programming by Contract (PEP 316)?

[Russ]

Paul Rubin wrote:
> Bruno Desthuilliers <bdesth.quelquechose at free.quelquepart.fr> writes:
> > FWIW, the "Eiffel and SPARK Ada folks" also "brilliantly explained"
> > why one can not hope to "write reliable programs" without strict
> > static declarative type-checking.
>
> I don't know about Eiffel but at least an important subset of SPARK
> Ada's DBC stuff is done using static analysis tools (not actually
> built into the compiler as it happens) to verify statically
> (i.e. without actually running the code) that the code fulfills the
> DBC conditions.  I don't see any way to do that with Python
> decorators.

Yes, thanks for reminding me about that. With SPARK Ada, it is
possible for some real
(non-trivial) applications to formally (i.e., mathematically) *prove*
correctness by static
analysis. I doubt that is possible without "static declarative type-
checking."

SPARK Ada is for applications that really *must* be correct or people
could die. With all
due respect, most (not all, but most) Python programmers never get
near such programs
and have no idea about how stringent the requirements are. Nor do most
programmers
in general, for that matter. (It's not an insult)