Between March 6th and March 13th 2019, I attended the Mirage retreat organized by Hannes Mehnert in Marrakesh, Morocco.
The Mirage retreat takes place in an artist residency organized as a hostel (shared rooms with simple beds). Hannes gathers a lot of people whose activity is relevant to the Mirage project; some of them work within the OCaml ecosystem (but not necessarily Mirage), some work on system programming (not necessarily in OCaml). The whole place is for all of us for one week, excellent food is provided, and we get to do whatever we want. (Thanks to the work of the people there who make this possible.)
This was my second time attending the retreat -- first time in November 2017. It is probably the work-related trip I enjoy most. When I get back home, I'm exhausted, thrilled, I met fascinating people and I learned a lot.
As part of my PhD at Gallium, I have been working on formally proving OCaml programs using Coq. More precisely, the focus has been on proving not only that a program is functionally correct (always compute the right result), but also does so in the expected amount of time. In other words, we are interested in formally verifying the asymptotic complexity of OCaml programs.
In this blog-post, I'm happy to report on our latest endeavour: the verification of the correctness and (amortized) complexity of a state-of-the art incremental cycle detection algorithm.
There are several ways of compiling a regular expression (RE) down to a deterministic finite-state automaton (DFA). One such way is based on Brzozowski derivatives of regular expressions. In this post, I describe a concise OCaml implementation of this transformation. This is an opportunity to illustrate the use of fix, a library that offers facilities for constructing (recursive) memoized functions and for performing least fixed point computations.
Last year (2017), I was following the MPRI, a research-oriented master programme in Paris. The project for the Functional programming and type systems course (taught by François Pottier, Didier Rémy, Yann Régis-Gianas and Pierre-Évariste Dagand) was to write a compiler for a tiny functional language. I extended that project with algebraic effects and a static type system checking that effects could not be unhandled. Explaining the type system of my implementation is what this post is about.
In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.
Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, ...), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.
In this blog-post, I would like to present what I think is one such situation. What the puzzle is, how we solved it, and why you shouldn't probably do that if you like spending your time in a useful manner.
Instructors of "Introduction to programming" courses know that students are willing to blame the failures of their programs on anything. Sorting routine discards half of the data? "That might be a Windows virus!" Binary search always fails? "The Java compiler is acting funny today!" More experienced programmers know very well that the bug is generally in their code: occasionally in third-party libraries; very rarely in system libraries; exceedingly rarely in the compiler; and never in the processor. That's what I thought too, until recently. Here is how I ran into a bug in Intel Skylake processors while trying to debug mysterious OCaml failures.
I have been asked whether an automatically-generated visitor, as produced by the visitors syntax extension for OCaml, can be used to construct an iterator.
It turns out that this can be done in a simple and efficient manner. (Up to a constant factor, the time complexity of this solution is optimal.) As the problem is interesting and its solution is somewhat nonobvious, I am describing them here.