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

Date: 30 Jun 2006 14:58:34 -0700

Message-ID: <1151704713.946895.228660_at_p79g2000cwp.googlegroups.com>

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