PROPOSAL: reflective kernel with a basic lisp

[Fare Rideau]

Jordan Henderson kindly proposed to manage proposals.
Here is mine:


PROPOSAL: Tunes architecture for LispOS: reflective kernel with basic lisp


SUMMARY:

We shall found the OS upon a reflective kernel.
Then, we can reflectively define whatever lisp dialects we want
and dynamically found their operational semantics
atop a very basic, low-level, lisp.
The most important concept being reflectivity,
which allows for this building.


NOTE:

This effort is independent from building an application base
in any existing language that we'll eventually support (CL, Scheme, *ML, etc).


A REFLECTIVE KERNEL:
* a Schemeish syntax for pure applicative lambda calculus
* first-class environments, continuations, and invariants.
* the ability to dynamically define
 the partial, abstract semantics (specification) of running objects
 without having to give their complete, concrete semantics (implementation).
* The ability to dynamically change the implementation of an object
 without modifying its specification.
* Hence, the ability to define exactly the lisp dialect needed
 for a particular task, and have it run, as long as it is well-founded
 on basic constructs, without being tied by the initial implementation used.


BASIC LISP:
* provides low-level primitives
* let's just reuse the fine work from ANS FORTH committee
 wherever low-level computational primitives are needed.
* we would use multiple-return-value instead of stack-based return,
 and multiple-continuations or lists instead of variable stack return size.
* For instance, add-with-carry would be:
 	(low-level::add-with-carry num1 num2 if-non-carry if-carry)
		=(if-non-carry (low-level::+ num1 num2))	if no carry
		=(if-carry (low-level::+ num1 num2))		if carry
* additional (control, float, whatever) stacks and memory are accessible
 through more primitives; side-effects are made available for these.
* so low-level that it doesn't have a builtin GC, type-checking, or anything.
* straightforward code generation possible so it runs on top of
 Flux, POSIX, raw hardware, or whatever you like.
* architecture-dependent stuff available through a built-in assembler,
 and yet other reflectively defined intermediate layers above the hardware.


BUILDING THE SYSTEM:
On top of the reflective kernel and the basic lisp,
modules would orthogonally implement:
* an generic invalidation/recovery system
 (useful for GC/Persistence barriers, code specialization, method dispatch,
 and anything that's logically a cache).
* an orthogonal persistent object store.
* a higher-order module/object system.
* an optimizing run-time code generator
 (in an orthogonally persistent system,
 any compilation IS run-time code-generation).
* bignums, ratnums, flonums (for architectures w/o FPU),
 quadraticextensionsnums, complexnums, quaternionnums, padicnums,
 symbolicalgebranums, ADAnums, wtfnums, booleans, etc.


STANDARD LANGUAGES:
* standard-conformant languages could be built completely on top
 of the reflective system.
* These include Lisp variants like Scheme, CL, elisp, EuLisp, Dylan, etc.
* Other interesting real languages might include
 OCAML, SML, Clean, Haskell, Prolog, Mercury, etc
* Lesser languages might include Modula-n, Eiffel, ADA, etc.
* Shitty languages might include C, C++, etc.
* Any implemented language allows to leverage the associated
 software legacy base,
 and to attract developers using these languages toward LispOS.
* Of course, LispOS developers could choose any clean intermediate step
 between the basic lisp and a standard lisp,
 using first-class invariants to specify just the needed features,
 and letting them be orthogonally implemented through reflection.


OTHER EXTENSIONS ALLOWED BY A REFLECTIVE SYSTEM:
* emulators for stupid low-level architectures (Unix, etc).
* a generic/formal GC generator.
* a software correctness proof system.


REFERENCES:

This looks quite like the Tunes project,
with the basic lisp being the Tunes LLL subproject,
http://www.eleves.ens.fr:8080/home/rideau/Tunes/Subprojects.html#LLL


SIGNATURE:

== Fare' -- rideau@ens.fr -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"