I do not support any standard language for describing systems.
Such a language seems just as difficult and controversial as a
standard verification language. It seems to me that, ideally, each system
developer should make some attempt to provide translators into and
out of other languages. In this way we can develop a distributed
"translation web". I think that over time a small set of standard
languages will become widely used as "interlingua".
I do not think that developers will choose to build translators to and
from raw set theory. Raw set theory does not maintain the "structure"
of theorems. Structure is essential in heuristically guiding
verification. For example, many verifications rely on type checking
algorithms. Raw set theory does not distinguish types from other
formulas.
I would also like to avoid centralized "certification" of the
soundness of systems. Unsound systems will get bad reputations.
Confidence in a theorem should be established by verifying it with
systems that have good reputations or by verifying it in several
different systems.
David