Asp Forum - optional static typing for Python

Russ P.

1/27/2008 10:19:00 PM

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/sta...

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.sourc...),
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.

40 Answers

Jarek Zgoda

1/27/2008 10:37:00 PM

Russ P. pisze:

> 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.

I thought it was april fools joke?

--
Jarek Zgoda
http://zgo...

"We read Knuth so you don't have to" - Tim Peters

André

1/27/2008 10:50:00 PM

On Jan 27, 6:19 pm, "Russ P." <Russ.Paie...@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/sta...
>
> 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.sourc...),
> 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... might be
relevant?
André

Russ P.

1/27/2008 10:53:00 PM

On Jan 27, 2:36 pm, Jarek Zgoda <jzg...@o2.usun.pl> wrote:
> Russ P. pisze:
>
> > 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.
>
> I thought it was april fools joke?

On January 21, 2000? Which calendar do you use?

Russ P.

1/27/2008 11:01:00 PM

On Jan 27, 2:49 pm, "André" <andre.robe...@gmail.com> wrote:
> On Jan 27, 6:19 pm, "Russ P." <Russ.Paie...@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/sta...
>
> > 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.sourc...),
> > 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-... be
> relevant?
> André

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

Jarek Zgoda

1/27/2008 11:09:00 PM

Russ P. pisze:

>>> 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.
>> I thought it was april fools joke?
>
> On January 21, 2000? Which calendar do you use?

Static typing in Python is usual theme of april fools jokes.

--
Jarek Zgoda
http://zgo...

"We read Knuth so you don't have to" - Tim Peters

Russ P.

1/27/2008 11:14:00 PM

On Jan 27, 3:08 pm, Jarek Zgoda <jzg...@o2.usun.pl> wrote:
> Russ P. pisze:
>
> >>> 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.
> >> I thought it was april fools joke?
>
> > On January 21, 2000? Which calendar do you use?
>
> Static typing in Python is usual theme of april fools jokes.

I hope Guido doesn't find out about that!

Arnaud Delobelle

1/27/2008 11:22:00 PM

On Jan 27, 11:00 pm, "Russ P." <Russ.Paie...@gmail.com> wrote:
> On Jan 27, 2:49 pm, "André" <andre.robe...@gmail.com> wrote:
> > Perhaps this:http://www.python.org/dev/peps/pep-31...
> > relevant?
> > André
>
> Thanks. If I read this correctly, this PEP is on track for Python 3.0.
> Wonderful!

Note that annotations do not provide explicit typing, AFAIK:

def f(x:int) -> int: return x*2

is stricly equivalent to

def f(x): return x*2
f.__annotations__ = {'x':int, 'return':int}

You still need to write a type-checking wrapper. PEP 3107 mentions two
such tools:
* http://oakwinter.com/code/...
* http://maxrepo.info/taxonomy/te...
Neither require annotations.

ajaksu

1/27/2008 11:29:00 PM

On Jan 27, 9:13 pm, "Russ P." <Russ.Paie...@gmail.com> wrote:
> On Jan 27, 3:08 pm, Jarek Zgoda <jzg...@o2.usun.pl> wrote:
>
> > Russ P. pisze:
>
> > >>> 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.
> > >> I thought it was april fools joke?
>
> > > On January 21, 2000? Which calendar do you use?
>
> > Static typing in Python is usual theme of april fools jokes.
>
> I hope Guido doesn't find out about that!

He does know, follow http://mail.python.org/pipermail/python-dev/2007-April/0...
and get a laugh too! :)

On a more serious note, I suggest you look up ShedSkin, Pyrex and
Cython, where the static typing is used for better performance. And
with Psyco, you get dynamic typing with JIT specialization. In core
CPython, little is being done AFAIK to support static typing per-se,
but annotations can (and probably will) be used for that end. However,
I don't think it'll interfere in how CPython executes the program.

Daniel

Christian Heimes

1/27/2008 11:40:00 PM

Arnaud Delobelle wrote:
> On Jan 27, 11:00 pm, "Russ P." <Russ.Paie...@gmail.com> wrote:
>> On Jan 27, 2:49 pm, "André" <andre.robe...@gmail.com> wrote:
>>> Perhaps this:http://www.python.org/dev/peps/pep-31...
>>> relevant?
>>> André
>> Thanks. If I read this correctly, this PEP is on track for Python 3.0.
>> Wonderful!
>
> Note that annotations do not provide explicit typing, AFAIK:
>
> def f(x:int) -> int: return x*2
>
> is stricly equivalent to
>
> def f(x): return x*2
> f.__annotations__ = {'x':int, 'return':int}

Your assumption is correct.

Christian

Paddy

1/28/2008 1:03:00 AM

On Jan 27, 10:19 pm, "Russ P." <Russ.Paie...@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/sta...
>
> 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.sourc...),
> 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.

If static typing is optional then a program written in a dynamic
language that passes such an automated static analysis of source code
would have to be a simple program written in a simplistic way, and
also in a static style.

Having used such formal tools on hardware designs that are expressed
using statically typed languages such as Verilog and VHDL, we don't
have the problem of throwing away run time typing, but we do get other
capacity problems with formal proofs that mean only parts of a design
can be formally prooved, or we can proof that an assertion holds only
as far as the engine has resources to expand the assertion.
We tend to find a lot of bugs in near complete designs by the random
generation of test cases and the automatic checking of results. In
effect, two (or more) programs are created by different people and
usually in different languages. One is written in say Verilog and can
be used to create a chip, another is written by the Verification group
in a 'higher level language' (in terms of chip testing), a tunable
randomized test generator then generates plausible test streams that
the Verification model validates. The test stream is applied to the
Verilog model and the Verilogs responses checked against the
Verification models output and any discrepancy flagged. Coverage
metrics (line coverage , statement coverage, expression coverage ...),
are gathered to indicate how well the design/program is being
exercised.

I would rather advocate such random test generation methods as being
more appropriate for testing software in safety critical systems when
the programming language is dynamic.

- Paddy.
P.S. I think that random generation has also been used to test
compilers by automatically generating correct source for compilation.

comp.lang.python

optional static typing for Python

Russ P.

Jarek Zgoda

André

Russ P.

Russ P.

Jarek Zgoda

Russ P.

Arnaud Delobelle

ajaksu

Christian Heimes

Paddy

x Login to ForumsZone