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<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 > > > > > > _______________________________________________ > fonc mailing list > [email protected] > http://vpri.org/mailman/listinfo/fonc >
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
