[nem-en] Formal Islands - safe macros

[Sandro Magi]

I think this will be of interest to Nemerle devs as it consists of a
sort of "safe, formal macro framework" built into the language:

Formal Islands

Abstract. Motivated by the proliferation and usefulness of Domain
Specific Languages as well as the demand in enriching well established
languages by high level capabilities like pattern matching or strategic
rewriting, we introduce the Formal Islands framework.

The main idea consists to integrate, in existing programs, formally
defined parts called Islands, on which proofs and tests can be
meaningfully developed. Then, Formal Islands could be safely dissolved
into their hosting language to be transparently integrated in the
existing user environment.

The paper presents this generic framework and shows that the properties
valid on the formal islands are also valid on the corresponding
dissolved host codes. Formal Islands can be used as a general
methodology to develop new DSL and we show that language extensions like
SQLJ—embedding SQL capabilities in Java—, or Tom—a Java language
extension allowing for pattern matching and rewriting—are indeed Islands
and they can therefore be used for formal software developments.

http://hal.inria.fr/docs/00/06/10/51/PDF/submitted-paper.pdf

Sandro