On Tue, Dec 19, 2000 at 10:26:57AM +0100, Sven LUTHER wrote:
> On Tue, Dec 19, 2000 at 07:23:35PM +1000, Anthony Towns wrote:
> > On Tue, Dec 19, 2000 at 09:43:27AM +0100, Sven LUTHER wrote:
> > > What about writing some kind of code that resolve the vote in some kind of
> > > easy to prove language, and then do some program property proofs on it ?
> > I'm not sure why this helped (because I didn't do it), but it did.
> Actually i was speaking of algorythm proofing using some kind of program
> prover. I am not an expert in the domain, but i know it has been used
> succesfully for various kind of stuff (like proving chip architecture, or
> automated train systems) .
Yeah, I know what you meant. Algorithm proving was completely impossible
to automate (you can automate *checking* the proof, which is helpful),
last I looked. Even for simple programs.
Cheers,
aj
--
Anthony Towns <aj@humbug.org.au> <http://azure.humbug.org.au/~aj/>
I don't speak for anyone save myself. GPG signed mail preferred.
``Thanks to all avid pokers out there''
-- linux.conf.au, 17-20 January 2001
Attachment:
pgpYLIHFt45t4.pgp
Description: PGP signature