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

lists at notatla.org.uk lists at notatla.org.uk
Thu Jan 27 21:05:36 EST 2005

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

> I think it's a third phase. Phase one is to have a language and some
> reason to believe that building a good proof environment is worth the

Can people suggest what good truly introductory stuff is there on s/w proofs ?

After a litle websearching I have the idea 
    "Introduction to HOL", M.J.C. Gordon et al, Cambridge U Press 1993 ISBN 0-521-441897]
might be a misleading title based on this review
that I don't understand.    OTOH
makes it sound more accessible.

Anther thing I've never managed to glean from the EROS site is what is the back-end
structure representing/enacting a capability ?  If I'm holding an opaque blob that
authorizes something is that an index to some kernel structure that can be viewed as
a definition writen in some language ?  If it's not a language with arbitrary
expressiveness doesn't that mean the designers have to envisage every possible
capability that might be wanted ?

Would adding some NVRAM make it easier to store all relevant capabilities
(up to the recent split second) and simplify the process persistance issue
that's being discussed on this list ?  Would it be acceptable to require an
NVRAM component in PCs for running Coyotos ?

More information about the coyotos-dev mailing list