Re: Sponsor this
On Tue, Dec 19, 2000 at 07:46:15PM +1000, Anthony Towns wrote:
> 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.
Yes, but they are lot of semi-automated proof systems, i think.
Anyway, i don't know if the use of such methods will be helpfull in solving
the voting problem, or if the use of algorythm language would be clearer for
debian developper and fit for inclusion in the constitution, in place of
textual stuff ?
Friendly,
Sven Luther
Reply to: