[
Lists Home |
Date Index |
Thread Index
]
At 10:12 27/08/2003 -0500, Hunsberger, Peter wrote:
>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.
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 :-)
regards DaveP
|
