Re: Bob's 'Self-aggrandizing ignorant' Count: Was: What databases have taught me

Bob Badour wrote:
>
> Absolutely. I have friends who have done real-time programming where the
> work had to be completed in assembler and where one had to prove the
> maximum number of CPU cycles consumed in the worst-case situation did
> not exceed some threshold.
>
> These observations naturally lead one to two important questions:
>
> 1) Can one create a pair of languages where the proofs written in one
> language establish the correct outcome and where some other language
> instructs the compiler on how to implement to get the best possible
> performance?
>
> 2) Could one create a compiler to translate proofs as above in 1) into
> assembler code with an automated proof that the maximum number of CPU
> cycles consumed in the worst-case situation would not exceed some threshold?
>
> These then lead into a third question: Can one combine the above
> features in a single product?

I see no particular theoretical difficulty. A type system could be designed
that would handle the above. What is necessary is that the type system have an accurate measure of the ceiling of every kind of node in the abstract
syntax of the language, parameterized on the child nodes.

Such a language could not be Turing complete, or perhaps could have a non-Turing complete subset. For example, one might allow a top level event loop that itself took infinite CPU cycles (in that it never terminates)
but each iteration through the loop was guaranteed to complete within some
upper bound of time. One could statically analyze any resource this way:
heap space, stack space, file handles, CPU time, etc.

The type system would be more than usually bound to a particular machine
architecture, but this detail could perhaps be abstracted out. So we could
prove that this program executes in less than 30 s. on a pentium, but that same proof would not be valid for a 486.

Marshall Received on Fri Jun 30 2006 - 23:58:34 CEST