A possible approach, on which I was experimenting some time ago, would be to use ephemerons to attach predicates to data, which could be later checked (a mere presence check) on the caller side.
Something like this:
let typecheck code =
ensures ["well-typed"] @@
let normalize code =
provides ["well-typed"; "normal-form"] @@
let optimize code =
requires ["normal-form"; "well-typed"];
provides ["normal-form"; "well-typed"; "optimized"] @@
requires tags obj is a function of type
string list -> 'a -> unit that takes a list of tags, denoting features, and checks that they are attached to the given object, and
provides tags obj is a function of type
string list -> object -> object takes a list of features and attaches it to the object (an alternative syntax is having type
object -> unit, since an ephemeron is a mutable hashtable).
The implementation is using ephemerons, which are hashtables indexed with arbitrary boxed objects with a special treatment of liveness (i.e., values from those hashtables disappear when the index disappear, so no memory leakage should happen).
The main benefit of this approach is its simplicity, it is vanilla OCaml, it is easy to implement, and easy to disable. The main drawback is that it works only with heap values (aka boxed values) and that it is not reflected in the function signature. And of course, since it is that simple, the contract can’t actually be a formula, especially that references the host language.