I noticed there are a couple of research projects that implement new language features for a contract language, but not seeing anything library-based for mainline OCaml. Is anyone doing it now or in did in the past? Wondering what people’s thoughts are. Personally, today I feel it should be possible to do with extension points. Maybe something like,
let divide x y = x / y
[@@dbc.pre "y <> 0"]
[@@dbc.post "result * y = x"]
Thanks for the pointer, I can’t seem to find anything in their repos though ( https://github.com/AestheticIntegration ).
Check out https://try.imandra.ai. It has a bunch of examples in Jupyter notebooks. There’s also the docs page https://docs.imandra.ai
Your example above would look something like this (with integer arithmetic, obv):
# let divide x y = x / y;;
val divide : Z.t -> Z.t -> Z.t = <fun>
# verify (fun (x, y) -> (y <> 0) ==> (((divide x y) * y) = x));;
- : Z.t * Z.t -> bool = <fun>
Counterexample (after 0 steps, 0.020s):
let _x = (1, 2)
[✗] Conjecture refuted.
module CX : sig val _x : Z.t * Z.t end
in the example above, you’ll notice the counterexamples are reflected back into the runtime, so you can directly compute with them:
# CX._x;;
- : Z.t * Z.t = (1, 2)
# let x, y = CX._x in divide x y;;
- : Z.t = 0
Wow, that’s cool! Although I’m actually looking for something slightly different, I’ll definitely try this out too, it’s quite impressive! 
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"] @@
perform_typecheck code
let normalize code =
requires ["well-typed"];
provides ["well-typed"; "normal-form"] @@
perform_normalization code
let optimize code =
requires ["normal-form"; "well-typed"];
provides ["normal-form"; "well-typed"; "optimized"] @@
do_optimizations code
where 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.
So the ephemerons are attaching to the function return values? I’ll need to dig a bit deeper but for the problem of ‘attaching arbitrary data to something’ I figured we could ask the user to do it themselves as part of their postcondition check:
let divide x y =
Dbc.pre ~message:(Printf.sprintf "%d > 0" y) @@ y > 0;
Dbc.pre ~message:(Printf.sprintf "%d >= %d" x y) @@ x > y;
let check = Dbc.post ~message:(Printf.sprintf " * %d = %d" y x) @@ fun result ->
result * y = x in
check @@ x / y
It’s not reflected in the signature and has a couple of other drawbacks, but is relatively simpler to implement.
The main design constraint when I was devising my approach is that the checks are heavy and it is not an option to validate inputs in runtime (e.g., type checking, different code normalizations, they are usually hard transformations, where the cost of an operation and the cost of the check whether this operation was applied is the same). If it weren’t true, then I don’t see any reason why a simple assert check couldn’t be used (or any other runtime checking framework, such as JS Validate and Quickcheck).
P.S. concerning my approach, it is basically a runtime alternative to phantom types which could be used in the same manner to annotate values with a set of predicates, but the inclusion is checked in compile time. Both approaches are valid, with the dynamic approach more attractive in cases where the set of predicates is big and/or open and/or when the interfaces are fixed, so you can’t change the types.
Ah I see, so your let-bindings are kind of like Clojure specs that would be run as part of a test suite, not at runtime of the actual application. They are conceptually closer to Imandra’s approach, actually. (Imandra is specifically checking the implication form precondition to postcondition is valid though).
No, vice verse, they will be actually run during the runtime, as assertions would. The requires and provides are normal OCaml functions. Ephemerons are used to prevent memory leaks (so that properties of a value do not outlive the value itself) and to ensure polymorphism (the 'a type).