I've been working for years on sidekick, on my free time. It's getting tiresome to put so much effort into a project in the dark, so here's some basic journaling/rambles about it.

So what's Sidekick? At first, and for a while, it was an attempt at writing a SMT solver, in OCaml, following the CDCL(T) paradigm, and in a functorized way. I've gone back on at least the last point, and the CDCL(T) part might be revisited soon.

(original title: "Curry Howard is a scam". See below.)

The Curry-Howard correspondence has been talked about a lot recently, not only in Haskell circles, but also among CiC-based proof assistant practitioners (Coq, Lean, etc.). In a nutshell, it makes a deep parallel between "programs" (terms of some flavor of lambda calculus, typically), and "proofs" (these programs are a proof of their type, or more precisely they are witnesses that their types are inhabited). The most basic example is id x = x which, in Haskell, would be a proof of $ \forall a. a \rightarrow a $, a trivial theorem of propositional logic.

That's all good and well, but my point here is that in practice, the equivalence is not as interesting as it first looks.

I've decided I want to resume blogging. So without further ado, here's a short piece about one of my side projects: benchpress (with a live hosting of the web ui).

In short, benchpress is a tool I use for running provers, by which I mean, generally, command-line tools that take a logic problem as input, and output something about the file such as "it's a valid theorem" or "it typechecks" or some sort of failure or timeout. The idea is to make it easy to run a tool you're developing (e.g. E, Zipperposition, Batsat, Archsat, etc.) on a large set of benchmarks, and analyze the results.

The glamorous world of SAT and SMT solvers is usually preoccupied with proving theorems, searching for software bugs, verifying hardware, and other similarly serious business.

But today, we're going to solve Sudoku grids. My goal is to showcase mSAT, a parametrized SAT solver written in OCaml by my good friend Guillaume Bury and myself. The solver's code can be found on github, but I'm going to detail the most salient parts here.

Last October, I moved in Nancy to start working as an engineer with Jasmin Blanchette on an exciting project called Nunchaku. Since my domain is formal logic, I spend a lot of time manipulating, transforming, and traversing ASTs (abstract syntax trees). My primary method for debugging is pretty-printing structures; in nunchaku, I even have a --print-all flag to print the AST after each transformation, since the tool is basically a bidirectional pipeline that composes transformations. I will certainly blog on the design of Nunchaku later, but today I want to present the standard Format module from OCaml, that I use for pretty-printing all my data structures.

Greating, earthlings! Today I will present an exciting new OCaml library called maki. This post will be longer as usual, because it is actually two posts in one:

• first, I'll present the goals of Maki, sketch its design, and present the most salient parts of its API;
• then I will demonstrate how to use it to quickly build a (very naive) OCaml build system, featuring parallel build and cached computations thanks to Maki.

A quick note about my current OCaml setup, in my last project, Nunchaku.