[coyotos-dev] Couple of potential-someday-user questions
smustudent1 at yahoo.com
Thu Jan 27 13:19:53 EST 2005
--- "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.
> 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
Do you Yahoo!?
Yahoo! Mail - now with 250MB free storage. Learn more.
More information about the coyotos-dev