[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: Sponsor this



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: pgpa2PSM4MMRc.pgp
Description: PGP signature


Reply to: