(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.

I have been hacking on the OCaml compiler recently; in particular, I added some support for coloring warning/error messages. At some point during the discussion over this pull request, it became clear that colored output should only be enabled if stderr was an interactive terminal (in opposition to a regular file handle or whatnot). The compiler does not link with the Unix library, so I finally decided to add a primitive caml_sys_is_interactive. My purpose here is to explain how it works (from what I gathered) and how to do it.