[coyotos-dev] Couple of potential-someday-user questions

[C Y]

--- "Jonathan S. Shapiro" <shap at eros-os.org> wrote:

> On Wed, 2005-01-26 at 19:27 -0500, Eric Northup wrote:
>
> I think there was a mis-reading here.
> 
> We are looking at ACL2, HOL, and Twelf as initial embedding
> environments where we can validate our ideas about the viability of 
> this degree of program proof.

Is that still in doubt?  I thought there were a couple of proofs done
for EROS that were successful - does Coyotos require a scale of proof
such that it is unclear whether it's possible?

> C Y is asking for something else. He is noting that no proof engine
> is likely to be perfect, and we need to be able to check their work.

Right.

> Fortunately, it doesn't matter if the proof tool is right -- only if
> the proof is right. *Checking* a proof produced by an imperfect tool 
> is actually not that hard. The best way to achieve what C Y is after 
> is to eventually provide a means for multiple proof *checkers* to be
> applied to a proof script produced by the BitC prover.

That's what I ment to say ;-).  Is that planned, or too much work to be
practical?

CY


		
__________________________________ 
Do you Yahoo!? 
Yahoo! Mail - now with 250MB free storage. Learn more.
http://info.mail.yahoo.com/mail_250