optional static typing for Python

[Russ P.]

On Jan 27, 5:03 pm, Paddy

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

Yes, but for safety-critical software you usually want the simplest
possible solution. The last think you want is an unnecessarily "fancy"
design. Unless there is a darn good reason to write a "non-static"
program, you just don't do it.

You might want to check into what the FAA allows in "flight-critical"
code, for example. I am certainly not an expert in that area, but I've
had a passing exposure to it. My understanding is that every possible
branch of the code must be fully and meticulously analyzed and
verified. Hence, the dynamic dispatching of ordinary object-oriented
code is either prohibited or severely frowned upon.

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

Random test generation methods can go a long way, and they certainly
have their place, but I don't think they are a panacea. Coming up with
a random set of cases that flush out every possible bug is usually
very difficult if not impossible. That was the point of the quote in
my original post.