RE: [xml-dev] XML CMM and ISO9000 compliance? - was A standard approach to glueing together reusableXML fragments in prose?

["Hunsberger, Peter" <Peter.Hunsberger@stjude.org>]

Dave Pawson <dpawson@nildram.co.uk> writes:

> >Exactly what do you mean by "proven"?  There are classes of 
> languages 
> >that are known as "provable", meaning that they have mathematical 
> >properties that allow one to always generate proofs that an 
> algorithm 
> >works or does not work for any algorithm written in those 
> languages.  
> >In general, with most languages (those you list) this is not 
> possible.
> >
> >One can talk about proving that an algorithm does what you claim it 
> >does.  One cannot talk about proving a language, since any Turing 
> >complete language is non-bounded...
> 
> 
> The military do.
>   E.g. 'prove' all paths through a program.

Perhaps they manage this, but if so, they aren't proving a language,
they are proving that they know all paths a particular algorithm can
take. (Though generalizing some of these programs as algorithms might be
generous)

>   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 :-)
 
Yes, as one of my profs. Touched on when he introduced the topic:
proving that all the paths through an operating system are known seems
unlikely at best....

> Mind you, it gets kind of critical when 'proving' the launch software
>   for a missile leaving an airplane wing :-)

Or Mars lander software; (whoops)...  Tests are often substituted for
proofs.  "Voting" software that takes 2 out of 3 results (sometimes from
differing implementations of the same algorithm on different hardware)
is another way around "proofs".  Proofs are hard and sometimes
impossible, so there are many ways to do without them.