optional static typing for Python

[André]

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é