Challenges for the HLL

[Fare Rideau]

In case anyone cares,

I more and more tend to think that strongly typed systems that can use
the Curry-Howard isomorphism are somehow "simpler" when it comes to
managing proofs. See Coq and NuPrl. They appeared effective in providing
the following fundamental aspects of programming together with proofs:
* functional abstraction/function application (lambda and apply)
* inductive definitions (term algebras and recursion)

However, existing such systems failed to provide a usable way to program
efficiently with states and resources, and to mix programs written in
different paradigms. The following features have been experimented in them,
thanks to a bit of ad-hoc reflection:
* quotient structures (forgetting implementation dependencies)
* unique resources (linear programming)
But though these two features above allows theoretical modelling and
reasoning about low-level stateful programming, they don't provide
an actual way to seamlessly connect this reasoning to actual code.



We need specifically reflective constructs, "semantic attachment",
to tie and untie several aspects of a same object in a stateful setting
(in a pure setting, everything is, and happens to be looked at or not).
Such attachment is as when you write a program and tell the computer:
"forget the source layout, and focus on the meaning, but don't forget
the source, either, and allow decompilation"; then you already have two
different aspects of the program (abstract source and concrete implementation)
to synchronize.

Now, because your program also interacts with the store and
the network (where is the source stored? where is the program executed?),
multiple other aspects appear. Every aspect has constraints, that should not
be broken by operations on other aspects without some notification and
appropriate synchronization measures (for instance, the GC should only be
run at safe GC points; a database entry should only be read
when in a consistent state, not as is in a transient inconsistent state
due to its being edited; if a real-time constraint breaks, operators should
be notified; if network communications fail, something must be done; etc).



It is the semantics of such attachment that remains to define properly,
in presence of multiple aspects.
Traditional "reflective" systems force you into merging those aspects
manually into a static linear hierarchy of meta(n)-objects,
where the highest modified meta(n) object constitutes the implementation.
However, such merge is already an overspecification and a computer's job.
in Tunes, we'd like to allow independent and dynamic specification
of multiple aspects. Well-founded computability of objects mean that
any two aspects in the dynamic hierarchy can be unified into a
more specific aspect that encompasses both of them; the hierarchy of aspects
must hence be dynamically included by the system in a lattice whose
most concrete element be the "actual implementation" that encompasses
all aspects.



Regards,

== Faré -=- (FR) François-René Rideau -=- (VN) Уng-Vû Bân -=- rideau@ens.fr ==
Join a project for a free reflective computing system! | 6 rue Augustin Thierry
TUNES is a Useful, Not Expedient System.               | 75019 PARIS     FRANCE
http://www.eleves.ens.fr:8080/home/rideau/Tunes/ -=- Reflection&Cybernethics ==