[
Lists Home |
Date Index |
Thread Index
]
You're right. For some systems, some proofs are worth paying for.
The question is which ones? Would it have been more useful for
NASA to have proven its low level engineers wrong about the
potential damage to the carbon edges or for the low level
engineers to have proven such damage is possible? The first
set would have been cheaper and answered the more immediate
question of what is the best course of action next. The
second set proves that what was theorized was possible and
probable. Nothing more. Given outcomes, I would have
preferred the first set of proofs.
For any proof to be meaningful, it must make a difference
to a choice of value. It must reduce uncertainty.
For proofs of XML to be valuable, we should know what choices
we are making.
It comes back to what is to be proven given the axioms of the
system and the rules for changing theorems to produce new but consistent
theorems if we are talking about formal systems. In fact, XML relies
heavily on the Draconian rule for rejecting non-well formed strings.
That's one level. What is proven? It doesn't prove XSLT will
operate as intended because XSLT operates on the infoset.
Does it prove that a correctly implemented XML parser can construct
a valid infoset?
What about operations on strings? Is XSLT proven to be lossless?
At what level?
One of the interesting issues of formal systems is how long one
can avoid discussing reality, the isomorphisms where meaningfulness
is found. As long as one is only discussing the system that is
defined by XML 1.0, one can do that virtually forever. The proofs
one would look for in your example are in the applications. Because
applications such as XSLT, XML Schema, XQuery and XPath are used
throughout the XML systems, proofs of these should be of interest
to all.
len
From: Dave Pawson [mailto:dpawson@nildram.co.uk]
The military do.
E.g. 'prove' all paths through a program.
Any stack based language fails on this basis,
hence Z was born as a KISS language,
to run on risc processors which were sufficiently simple to
enable 'proof' of this nature.
Or at least that's what the UK MoD tell us :-)
Mind you, it gets kind of critical when 'proving' the launch software
for a missile leaving an airplane wing :-)
|
