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
