optional static typing for Python

[Russ P.]

On Jan 27, 2:49 pm, "André" <andre.robe... at gmail.com> wrote:
> On Jan 27, 6:19 pm, "Russ P." <Russ.Paie... at gmail.com> wrote:
>
>
>
> > A while back I came across a tentative proposal from way back in 2000
> > for optional static typing in Python:
>
> >http://www.python.org/~guido/static-typing
>
> > Two motivations were given:
>
> >     -- faster code
> >     -- better compile-time error detection
>
> > I'd like to suggest a third, which could help extend Python into the
> > safety-critical domain:
>
> >     -- facilitates automated source-code analysis
>
> > There has been much heated debate in the past about whether Python is
> > appropriate for safety-critical software. Some argue that, with
> > thorough testing, Python code can be as reliable as code in any
> > language. Well, maybe. But then, a famous computer scientist once
> > remarked that,
>
> > "Program testing can be used to show the presence of bugs, but never
> > to show their absence!" --Edsger Dijkstra
>
> > The next step beyond extensive testing is automated, "static" analysis
> > of source-code ("static" in the sense of analyzing it without actually
> > running it). For example, Spark Ada is a subset of Ada with
> > programming by contract, and in some cases it can formally prove the
> > correctness of a program by static analysis.
>
> > Then there is Java Pathfinder (http://javapathfinder.sourceforge.net),
> > an "explicit state software model checker." The developers of JPF
> > wanted
> > to use it on a prototype safety-critical application that I wrote in
> > Python, but JPF only works on Java code. We considered somehow using
> > Jython and Jythonc, but neither did the trick. So they ended up having
> > someone manually convert my Python code to Java! (The problem is that
> > my code was still in flux, and the Java and Python versions have now
> > diverged.)
>
> > In any case, optional static typing in Python would help tremendously
> > here. The hardest part of automated conversion of Python to a
> > statically typed language is the problem of type inference. If the
> > types are explicitly declared, that problem obviously goes away.
> > Explicit typing would also greatly facilitate the development of a
> > "Python Pathfinder," so the conversion would perhaps not even be
> > necessary in the first place.
>
> > Note also that, while "static" type checking would be ideal,
> > "explicit" typing would be a major step in the right direction and
> > would probably be much easier to implement. That is, provide a syntax
> > to explicitly declare types, then just check them at run time. A
> > relatively simple pre-processor could be implemented to convert the
> > explicit type declarations into "isinstance" checks or some such
> > thing. (A pre-processor command-line argument could be provided to
> > disable the type checks for more efficient production runs if
> > desired.)
>
> > I noticed that Guido has expressed further interest in static typing
> > three or four years ago on his blog. Does anyone know the current
> > status of this project? Thanks.
>
> Perhaps this:http://www.python.org/dev/peps/pep-3107/might be
> relevant?
> André

Thanks. If I read this correctly, this PEP is on track for Python 3.0.
Wonderful!