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.
In two previous blog posts (part 1 and interlude), I presented a set of notions to prove asymptotic complexity of OCaml programs, then an OCaml implementation of Okasaki’s “binary random access lists”. In this last blog post, I combine the two ideas, and present a formalization of binary random access lists, using CFML.
This small interlude post is not about Coq nor CFML: I present a data structure from Okasaki’s Purely functional data structures, implemented in OCaml.
It comes as a preliminary explanation for an incoming formalization of it in CFML (see next post), including an complexity analysis!
In a recent paper, Arthur Charguéraud and François Pottier present a formal proof of an OCaml implementation of Tarjan’s union-find algorithm. The proof covers two aspects: first, functional correctness (“the algorithm is correct”), but also asymptotic complexity. For example, one of the results of the paper is that the
link function runs in \(O(α(n))\) elementary steps, \(α\) being the inverse of the Ackermann function.
Actually, the complexity results of the paper are not presented using the “big-O” notation, commonly used in asymptotic complexity proofs: the various constants are explicit and manipulated through the proof.
In these blog posts (current, interlude and final), I’ll describe a tentative extension of CFML, the Coq library François and Arthur used for their proof. Its goal is to enable asymptotic reasoning, big-O notations and such to be used to prove complexity of programs.
Coq offers several internal evaluation mechanisms that have many uses, from glorious proofs by reflection to mundane testing of functions. Read on for an account of my quest to get large parts of the CompCert verified C compiler to execute from within Coq. It was a mighty battle between the forces of transparency and opacity, with the innocent-looking “decide equality” tactic as the surprise villain…