optional static typing for Python

[Paddy]

On Jan 28, 1:56 am, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> Paddy <paddy3... at googlemail.com> writes:
> > 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.
>
> That method totally failed to find the Pentium FDIV bug, and they use
> static proof checkers like ACL2 now.

I would doubt that they would use purely static methods to verify such
large and complex chips. You need a spread of methods, and some
techniques find more bugs at different stages of the design. When
alerted to the existence of a bug then you have to create a test find
it and might well choose to create assertions for formal proof on that
section of the design.

Given the complexity of current microprocessors i'm guessing that
their previous testing methods would be too good to just junk in
totality because the FDIV bug was not found. Similarly if they were
not using formal methods then it makes sense to add it too your
arsenal; and unfortunately it takes a mistake like that to allow
different methods to be explored and incorporated.
It's rarely either/or. More a question of the right, cost-effective,
mix of tools to find bugs, and get the product released on time.

- Paddy.