OSEC

Neohapsis is currently accepting applications for employment. For more information, please visit our website www.neohapsis.com or email hr@neohapsis.com
Crypto Archives: Re: Testvectors

Re: Testvectors

Ben Laurie (benalgroup.co.uk)
Mon, 06 Sep 1999 16:02:49 +0100

Mike Roberts wrote:
>
> I seem to remember some work done at Oxford under Tony Hoare's
> "Communicating Sequential Processes" moniker in the late 80's. Essentially
> you formally combined known correct pieces of code from the ground up.
> Being constructive rather than deconstructive it didn't suffer from being
> uncomputable, but at the same time I don't think it was very easy to use,
> either ;) But I do think that that it proved that the correctness proof is
> not necessarily Halting problem like (when approached from the opposite
> direction), which is I think what was wanted ?

There is not a known way to avoid uncomputability without also removing
the ability to compute some computables things. Unfortunately, it isn't
known how to prove this, either, though if you can prove Church's
Thesis, you are away...

> Some work was done on proovably correct embedded microprocessors for the UK
> Military based apon it, but that's even hazier.

They gave up, coz it was too difficult (which doesn't surprise the
professional programmer in me in the slightest).

Cheers,

Ben. 

--
http://www.apache-ssl.org/ben.html

"My grandfather once told me that there are two kinds of people: those
who work and those who take the credit. He told me to try to be in the
first group; there was less competition there."
     - Indira Gandhi

This archive was generated by hypermail 2.0b3 on Mon Sep 06 1999 - 13:25:59 CDT