Lambda the Ultimate

Modular Verification of Code with SAT (pdf)

"For this case study, we used a pre-existing specification of the Java List interface written in the Java Modeling Language (JML) ...
an approach to checking object-oriented code against detailed specifications that is fully automatic, demanding from the user only a specification of the method to be checked, an indication of the size of the space to be searched, and for each distinct representation, an abstraction function and representation invariant."

Using Alloy's Kodkod - a new relational engine designed to be a plugin component / backend for other tools. (It solves Sudoku too...)

Let's suppose you have a language feature that only some code should have access to. For instance, Intensional Type Analysis/Reflection (ITA) can break abstraction barriers. Sometimes this sort of abstraction breaking is desirable, such as in generic pickling/serialization, printing, etc. but often it is not (violates parametricity theorems).

However, if we expose ITA as a language construct, then there are no restrictions on its use. So what we want is controlled abstraction breaking.

One solution is that ITA is exposed as a runtime provided object/module called Inspector. Inspector's signature has no constructor, so there is no way to construct an instance of it. Instead, an instance of Inspector is member of a standard set of such runtime objects that are provided to "main" and defines the "initial state of the world". "main" can then delegate access to Inspector to any code it deems should have it.

This is a capability design. However, I'm wondering if there's some way to express this constraint within the language itself, instead of resorting to a design pattern. In other words, keep ITA as a language construct, but somehow be able to express when it is legal to use ITA.

As an example of a possible solution, suppose we have a process language and two process constructors, one of which permits ITA expressions within it, the other of which doesn't:

expr  ::= process(expr) | lexpr | ita(expr)
lexpr ::= confined(lexpr) | ...

So a confined process cannot create an ordinary process or invoke ita. However, the composibility of the runtime Inspector object seems greater. Are there any other possibilities?