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
