I came to software through low-level development, with more than 10 years of C++ (video games and related systems). Unsatisfied by the complexity and unreliability of the software I wrote, I felt the urge to explore the theoretical foundations behind it: algebra, set theory, category theory, and formal modelling tools (TLA+, Coq/Rocq). I came to the conclusion that no problem can be solved satisfactorily, in terms of simplicity, reliability, efficiency and composability, without both understanding its underlying formal structures and having a good grasp of what is technically feasible. Reconciling theory and practice is what I find fascinating about this field.

• I like the correct-by-construction approach, as explained in the article Faultless systems: yes we can!. This involves modelling the system iteratively with increasing detail, proving key properties and proving that each model refines ("implements") the higher-level model.

• I also find the work of Conal Elliott inspiring, for its emphasis on simplicity and composability.

You can reach me at [email protected]