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.
I am no longer an official member of Gallium, but of course Gallium will always remain dear to my heart. And it is with a mix of sadness and anticipation that I’ve started writing articles on another blog, namely, the F* blog. If you wish to hear the latest news about F*, and chat about language issues, or just get a sense of what’s happening, you can go out there and start lurking in the comments section.
Looking forward to some bikeshedding^W constructive discussions!
In Merging OCaml Patches I wrote a description of my personal process to merge OCaml patches (usually submitted as github pull requests) in the upstream repository (currently SVN). This description may be useful for external contributors to understand the process, and maybe meet me halfway by doing a bit of the work upfront.