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<http://www.lix.polytechnique.fr/%7Ejouannaud/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
