SprintTODO: move any useful information about the Sprints from the old Wiki page
Ok, so once in a while, we'll organize a Tunes Sprint so as to speed up development by bringing together the focused attention of many contributors on some hot subject.
First sprint is sunday 2002-09-01 (that's today). It will start at 09:30 French time (07:30 UTC, 00:30 US/Pacific time), and finish 12 hours from then. This page will show progress, and so will IRC logs from #tunes on irc.openprojects.net.
Armin and I (Faré) are both in Paris, and we intend to define some core for the metaprogramming infrastructure: a MOP for defining and using Linear Graph Reduction virtual machines. Ideally, the specification will result in a test suite that can be used to check the (partial) correctness of the implementation that we intend to do in the coding sprint, beginning two weeks afterwards.
See these notes by Armin: http://bespin.org/~arigo/.
Additional notes by Faré: Need to distinguish between compile-time meta-level and run-time meta-level. Two different prefixes should be used instead of the same "meta". The "ultimate" compile-time meta-level ought to be a reflective framework. The "ultimate" run-time meta-level is the bare underlying hardware.
Water suggests to consider AP5 for relational specifications, Maude and BOBJ for rewrite logic, TIGRE for Graph Reduction implementation, and more... Maybe merging Maude and BOBJ already gives most of what we need? Read the Maude book "Reflection in Rewriting Logic".
- synchronize to some state that is meaningful for interpretation as a higher-level graph (as specified by the source code)
- "serialization" or otherwise interpretation into actual data structures interpretable at the higher abstraction level
- enumerating the "ports" of the graph, i.e. links between internal nodes and external graphs
- applying some evaluation rules (internal transformations and communication)
- reactivating the graph with some given strategy using the above rules
- listing invariants of the graph (preconditions and postconditions)
- listing "variants" of the graph (i.e. some rules that constrain the way the graph must progress from now to further observable stops)
1,2, and 3 are completely related to allowing meta-level compile-time correspondances, without having to stop compilation at some virtual machine that hardwires the abstraction level to a given graph representation.
Armin: one of the goals is to be able to specify integers as Peano integers, yet have an efficient bignum implementation, in a way that allows for reasoning to take place at the Peano level. Faré: i.e. as was done in Weyrauch's FOL.
The summary of what we came up with at the sprints is at http://bespin.org/~arigo/notes2.html.