SLUG Mailing List Archives
Re: [SLUG] Re: dynamic vs static type checking
- To: QuantumG <qg@xxxxxxxxxxx>
- Subject: Re: [SLUG] Re: dynamic vs static type checking
- From: Benno <benjl@xxxxxxxxxxxxxxx>
- Date: Tue, 27 Sep 2005 17:11:18 +1000
- Cc: slug@xxxxxxxxxxx
- User-agent: Mutt/1.5.9i
On Tue Sep 27, 2005 at 17:01:55 +1000, QuantumG wrote:
>Speaking of static analysis. I managed to get an evaluation version of
>It works by changing the level of representation at which you write
>software. Instead of writing imperative programs you write declarative
>specifications. The problem is it's:
> 1. a new, unfamiliar and difficult to master syntax (and way of
> 2. useless for already developed software.
> 3. limited in obscure and unobvious ways.
>In particular, you can write a full and complete specification, ask it
>to generate a program which implements that specification and it will
>barf. You've done everything that should be required but the state of
>the art of specification refinement that Perfect Developer embodies is
>not sufficient to generate code for any given specification. So you
>have to write code to do the "hard bits" of the specification, stating
>how the program should operate, not just what the program should do.
>That'd be fine if you could do it in a real programming language, but
>instead you've gotta use the specification language. Programming in a
>specification language is much like chinese water torture.
>But it gives you an idea of just how extreme static analysis can be.
>You literally can write some specifications in Perfect Developer that
>can be verified for internal consistency, automatically refined into a
>working prototype with good performance and deployed as is. Maybe in 10
>years time all critical systems will be written with tools like this?
>Maybe in 20 years time all other software will be written with tools
There is also Isabelle: http://isabelle.in.tum.de/ which is free.
And there is current work attempting to use such an approach to generate
a verified operating system kernel:
There is also splint, but that is a more traditional static analysis tool.