Rationale I'm starting a PhD on first-order automated theorem proving, which is the reason I'm writing an experimental theorem prover in OCaml. Theorem provers are full of complicated algorithms (that I plan to write on later), and my usual techniques for debugging are twofold: Writing a lot of assert to make sure invariants are not broken Printing debug information on stdout, if required, to get an idea of what the prover is doing. This allows me to choose the level of detail of what is prin...
