09:25 <Anarchos> What is the good framework to mimic first-order theories, and meta-theorems about their demonstrations in OCaml ? I tried modules and functors, but i wonder if classes would be better . What do people in the formal logic field use ?

12:30 <companion_cube> You mean to reflect proofs in ocaml itself?

12:36 <Anarchos> yes (i try to code all the Bourbaki proofs, except those with the hilbert operator), to write a verifier. But i also want theories to be parametrized by their signatures, and the possible to consider temporary adjunction of a theorem (for hypothesis adjunction style of demonstration).

13:24 <companion_cube> my advice is to not tie the verified to whatever language it's implemented in

16:53 <discocaml> <lukstafi> It sounds like you are focusing on recent history? If not:

16:53 <discocaml> <lukstafi> May 1996: OCaml 1.0 adds Object Oriented features to Caml Light Special.

16:53 <discocaml> <lukstafi> August 1998: OCaml 2.0 rewrites the class sublanguage to make it more logical, expressive and convenient.

16:53 <discocaml> <lukstafi> December 1999: OCaml 3.0 adds labeled and optional arguments (developed earlier as Objective Label), and polymorphic variants. (Non-beta in 2000.)

16:53 <discocaml> <lukstafi> October 2012: OCaml 4.0 adds GADTs (and enhances first-class modules, added in OCaml 3.12).

16:53 <discocaml> <lukstafi> December 2022: OCaml 5.0 adds a multicore runtime and effect handlers.

21:01 <discocaml> <astreamingcomesacrossthesky> if I need to expose a module from a library that it needs internally but I don't use myself, what's the best way to do that? I'm using `dune` and I thought adding the library to my `libraries` stanza would suffice, but that doesn't work...and I can't `open` the module and then leave it unused, afaik?