As part of my PhD, I’m writing an MLS implementation in F*. Such a specification allows to do proofs on MLS (such as security proofs or proof of correctness).
As a dependency of MLS*, I needed a library to implement parsers and serializers for the various message formats of MLS, with correctness proofs. I couldn’t use EverParse for technical reasons (namely, the fact that the theorems proved by EverParse do not work with DY*’s symbolic bytes). This is why I developed Comparse, which is a nice self-contained proof pearl: it relies on the modest amount of 2 basic message formats and 5 message format combinators, which are powerful enough to generate many message formats we may find in real-world cryptographic protocols (such as TLS 1.3, MLS or cTLS).
To help me and my roommates organize our chores, I designed some kind of shared todo-list manager for tasks that must be done on a regular basis. It computes the time you have to work each week for those tasks, helps you find which tasks have the highest priority, and helps you sharing the workload equally between peoples.
As part of my PhD, I found a security problem on MLS, under the condition that two different structures could be serialized to the same sequence of bytes. Rather than staring at the structures definitions long enough to find a collision, I figured that writing some dirty C++ to do the job for me would be more fun! In this code I heavily use templates, probably under the influence of my experience with F* and habits of using dependent types.
During high-school, I wanted to make a Rubik’s cube website with a friend. Of course, as a fellow yak shaver the first step to do this was obviously to write a WebGL Rubik’s cube renderer (at the time, the only Rubik’s cube renderers were written in Java applets which were starting to become obsolete). The website never saw life, however I did use this library to code a two-side PLL recognition trainer.
During high-school, we wanted to create a Rubik’s cube solver robot with some friends. I wrote a Rubik’s cube solver using Kociemba’s algorithm. The algorithm works in two phases. First, find a sequence of movements to put the cube in a state where it can be solved only with half-turn, except for the upper and lower face, Then, solve the cube with the new allowed movements. Both phases are solved optimally using the IDA* graph search algorithm. I also wrote a computer vision algorithm to scan a Rubik’s cube state using a webcam. Unfortunately, even though the algorithm was working great, the robot never worked.
During high-school, I played a lot with the Brainfuck programming language. I found it was slightly annoying to write because you constantly have to remember where on the memory band you are. To solve this problem, I developed a slightly higher-level language that compiles to Brainfuck. I didn’t know anything about compilers at the time, so it features a (not so buggy) hand-crafted parser in C++!