what kind of assertions are needed for a multi-processing proof system?

[rdm@tad.micro.umn.edu]

It seems to me that proofs are going to have to consider the data
being processed, as well as the code which is running.

Therefore, it's not completely true that the cost of a proof system is
going to be constant -- in an arbitrarily complex system it may have
to do arbitrarily complex data analysis before letting the
appropriate code run.

Or, what kinds of axioms is this proof system boing to be based on?

-- 
Raul