If I've got this right, Xavier wrote and proved the compiler in Coq, with one exception which was proved in a proof checker (aka verifier) - itself verified in Coq.
In this instance, Coq needs to be proven correct ie. it doesn't have any bugs itself, and Coq is a large program. So, the process is (lifting this mightily from http://objectmix.com/compilers/37124-compiler-correctness.html): 1. You develop your proof interactively with the prover (Coq). 2. You dump out the proof and run your proof checkers on it. 3. If it says your proof is good, then you're done. 4. If it says your proof is bad, then you curse, and fix the bug in the theorem prover and redo your proof. That's fine, but it is a lot of work. What I'm aiming at is a large amount of circularity so you can verify the prover in itself (and thereby be able to use a large amount of automation) via the route: prover specification => compiled by compiler written in prover => prover proves compiler correct => compiles certified prover. Substitute VM for compiler and you get a circular arrangement for establishing a proven baseline on particular hardware, and you can just rerun the proofs per machine to verify each one. As all subsequent code runs on the VM, you're much better off in terms of verifying this code. As for an OO browser take on an OS, I'm assuming you've looked at mobile maude (maude.cs.uiuc.edu/papers/postscript/principlesmm.ps.gz) - it is written with maude which means the debugger is available for (the fully distributed) testing. Mobile maude is based on mobile objects (carrying own internal state and code with them) and processes (located computation environments where mobile objects can reside), and uses async secure message passing between objects, together with a resource allocation mechanism. As objects can encapsulate the whole maude language, you get your fine-grainedness for free via the module structure. Personally, I think that mobile maude solves most of the issues you've been talking about. I'm trying to find a way to integrate maude with an OS in a useful way, so that these facilities are available on a global system scale. Cheers, Alexis. On 21 July 2011 22:31, John Zabroski <[email protected]> wrote: > This may be a case of my thoughts being more detailed in my head than > outwardly confessed. Sometimes I keep full design ideas in my head for > years at a time. > > But the thread I was thinking of was "On Inventing the computing > microscope/telescope for the dynamic semantic web" and my reply [1]. I > wrote a series of replies in that thread, but [1] is the specific one I > pulled from memory. > > By the way, do not read my comments about Smalltalk live images as a "value > judgment" on Dan Ingalls designs. He is an infinitely better software > designer than me. I am just provoked by Alan Kay's ideas on what a Web > Browser could look like if it was "object-oriented". I am surprised by how > many people I talk to do not see the rich criticism of modern web browsers, > and instead just hear Alan's comments as just another rant indistinguishable > from a teenager on Reddit. (I've also read commentaries in the past that > suggest Alan is more geared towards his Dynabook vision, whereas Dan is more > geared toward Doug Englebart-like "experimentation and prototyping", and > that the design of Smalltalk is ultimately the result of the fact that Dan > was the architect.) > > To me, solving secure code distribution means solving it, generally and > correctly (no bugs). That means taking into account things like > compression. > > Just to be clear, we're also looking for fine-grained distribution. We > already have the ability to ship operating systems around the Internet - > that's variously called "vMotion" or "live migration" or whatever. That's a > cheap parlor trick. Building infrastructure in such a way that you can > actually browse the state of the system and retrieve different > representations of the code is different. In particular, debugging > distributed code should really just be a special case of code distribution. > > From an optimization perspective, I want the software equivalent of what is > going on now in the Storage Area Network (SAN) space with things like > "tiering" data storage and integrated, check-box-simple tier optimization > like those Compellant offers. Alan pointed me to Gerry Popek's LOCUS > Distributed Operating System project, which I have been reading. > > Craig's project is straight-forward but targeted at a different concern, and > less general - but he also has WORKING CODE. I've been so tired lately > after work that I stopped most of my online activities like blogging, > posting to forums, including LtU. The idea being to focus on these personal > projects ideas. > > > [1] http://www.mail-archive.com/[email protected]/msg01451.html > > On Thu, Jul 21, 2011 at 8:25 AM, Alexis Read <[email protected]> wrote: >> >> I have to confess, I've looked through your previous posts and I can't >> find them - did you post to LtU, and could you supply some links? >> Just extrapolating now, I'm assuming you don't advocate Smalltalk as a >> good target for porting due to this image distribution problem. Craig >> Latta's Spoon project attempts to solve this, but I'd be interested to >> see your suggestion for a porting target. >> Thanks >> >> On 20 July 2011 22:15, John Zabroski <[email protected]> wrote: >> > Yes. Secure code distribution is not feasible with Smalltalk live >> > images >> > as-designed. Ergo, you cannot have a true distributed object-oriented >> > browser. >> > >> > On Wed, Jul 20, 2011 at 3:42 PM, Kevin Driedger >> > <[email protected]> >> > wrote: >> >> >> >> What is "Dan Ingalls' Smalltalk "live image" problem"? I'd very much >> >> like >> >> to hear about it. >> >> Is it in reference to images have their own set of problems wrt to >> >> dragging around more than just source code and being tightly coupled to >> >> the >> >> development environment that created them? >> >> ]{evin >> >> On Wed, Jul 20, 2011 at 3:33 PM, John Zabroski <[email protected]> >> >> wrote: >> >>> >> >>> Did you happen to read the posts I wrote on using Xavier LeRoy's >> >>> certified compiler building methodology to create a "object-oriented >> >>> browser" that doesn't succumb to Dan Ingalls' Smalltalk "live image" >> >>> problem? >> >>> >> >>> On Fri, Jul 15, 2011 at 5:36 PM, Alexis Read <[email protected]> >> >>> wrote: >> >>>> >> >>>> I've been looking at integrating formal methods, advanced typing and >> >>>> provability into STEPS, mainly as a good solution to being able to go >> >>>> from specifications to testable prototypes easily. I've been looking >> >>>> at a number of different languages and proof assistants that could >> >>>> fill the role. >> >>>> >From the (little) reading I've done, there seems to be a concensus >> >>>> that higher order languages/provers are more useful than first order >> >>>> ones, in particular, pattern matching for types/solutions appears to >> >>>> be more complete under higher order logic. >> >>>> For example, Epigram (http://www.e-pig.org/darcs/Pig09/web/) is based >> >>>> on dependent types, but uses first order matching and is incomplete >> >>>> (see the literal programming manual, Epitome, p163) ie. it doesn't >> >>>> neccessarily match all types/terms. I'm of the opinion that, although >> >>>> having a sound and complete parser/matcher is pretty useless >> >>>> day-to-day (most computer languages and systems are unambiguous), it >> >>>> is important to be sure you'll catch all types/terms for proofs and >> >>>> for execution. >> >>>> >> >>>> Coq, Isabelle and PVS all now use rewriting to some extent, though in >> >>>> a higher order fashion (ie. more general than lambda calculus eg. >> >>>> Curry-Howard calculi, dependent types). They do appear to use >> >>>> first-order logic for some proofs where decidability is a problem >> >>>> (www.lix.polytechnique.fr/~jouannaud/articles/tyl.pdf) and having >> >>>> seen >> >>>> some higher-order developments within Maude, I'd venture that it is >> >>>> useful to build higher-order provers on first-order environments - >> >>>> case in point, Epigram compiles down to Haskell constructs. >> >>>> >> >>>> There's a very good paper on pure type systems in Maude, with a view >> >>>> to implementing a higher-order (Open) Calculus of Constructions. The >> >>>> paper mentions a nice CINNI notation which allows you to use named >> >>>> types, rather than say de Brujin indices, and still avoid accidental >> >>>> type/term hiding. The proof assistant for OCC has been designed for >> >>>> use in a universe heirarchy >> >>>> >> >>>> >> >>>> (http://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr/occ_eng.html) >> >>>> which does sound similar to Alessandro Warth's Worlds POV. >> >>>> >> >>>> A later paper on the system is here: >> >>>> http://www.arnetminer.org/viewpub.do?pid=882439 It looks interesting, >> >>>> but I don't have a direct link for download unfortunately. >> >>>> Lastly, I've a couple of links to a declarative debugger in Maude - >> >>>> yes you can debug the specifications! >> >>>> (http://maude.sip.ucm.es/debugging/ and >> >>>> http://maude.cs.uiuc.edu/papers/pdf/Riesco-et-al-debugging-tr.pdf) >> >>>> >> >>>> Fairly recently, the Maude team (and contributors) wrote a formal >> >>>> analyser for java programs (JavaFAN - see the slides in the Maude >> >>>> intro http://maude.cs.uiuc.edu/talks/maude-padl10-slides.pdf). The >> >>>> basic strategy I've come up with, involves writing a version of Maude >> >>>> on top of Squeak (smalltalk), then adapting JavaFAN to analyse >> >>>> smalltalk bytecodes so you can prove the version of Maude itself, the >> >>>> VM, and thus the entire software stack from the top, down to the >> >>>> metal >> >>>> by virtue of running on the VM (ok, SqueakNOS isn't strictly bare >> >>>> metal, but STEPS/FRANK/NotSqueak should be, and I'd try to move the >> >>>> Maude runtime across). >> >>>> >> >>>> The Maude port would be straight - I don't know smalltalk that well, >> >>>> and I'm starting work by moving over the BuDDY library into Squeak. >> >>>> I'd appreciate people's thoughts on my programming direction. >> >>>> >> >>>> Cheers, >> >>>> Alexis. >> >>>> >> >>>> _______________________________________________ >> >>>> fonc mailing list >> >>>> [email protected] >> >>>> http://vpri.org/mailman/listinfo/fonc >> >>> >> >>> >> >>> _______________________________________________ >> >>> fonc mailing list >> >>> [email protected] >> >>> http://vpri.org/mailman/listinfo/fonc >> >>> >> >> >> >> >> >> _______________________________________________ >> >> fonc mailing list >> >> [email protected] >> >> http://vpri.org/mailman/listinfo/fonc >> >> >> > >> > >> > _______________________________________________ >> > fonc mailing list >> > [email protected] >> > http://vpri.org/mailman/listinfo/fonc >> > >> > >> >> _______________________________________________ >> fonc mailing list >> [email protected] >> http://vpri.org/mailman/listinfo/fonc > > > _______________________________________________ > fonc mailing list > [email protected] > http://vpri.org/mailman/listinfo/fonc > > _______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
