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 <[EMAIL PROTECTED]> <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
pgptIED8lzC4L.pgp
Description: PGP signature
