A sneak peek into my personal development methodology. TL;DR: Debugging is painful, unnecessary, and a sign of a poor design.

A story

Once upon a time, I was working on a project consisting of code written in two main programming languages: OCaml, and Rocq. To link the two parts, I used a generator of the former from the latter. Since the two languages have different type systems, the generator often had to emit code that was bypassing the type system of OCaml (using the type-casting function Obj.magic); however, all was fine, since the generator was well-tested (it was the standard OCaml extraction pipeline of Rocq).

Some of the code that I have manually written in OCaml also had to interface with Rocq-generated code. Since the interface was written in Rocq where I had the luxury of using dependent types (and dependent records), but the OCaml-based client code had to work with a less expressive type system, I had to insert a few type-casts now and there. All worked well, until…

One day I was working on a large feature. Actually, it was more than one day (rather a week); when the feature was done, I run some end-to-end tests and the software crashed. Of course, it was the fault of some type-cast. But which one? I spent some time trying to figure it out, but the OCaml code used lots of polymorphism, and that made debugging rather complicated. At some point I gave up and resorted to a different solution: I will rewrite the interface so that no type casts are necessary.

That seemed to me as a rather large endeavour, since all my Rocq code used dependent types quite heavily. The trick was in expressing the Rocq-OCaml interface without using dependent types, but keep using these in the depths of my Rocq code. So I re-designed the interface, adapted all the Rocq code, and moved on to adjust the OCaml code. Of course, during the process, I discovered which type-cast was at fault. But at that point, there was no need for any of these.

It is worth noting that the cognitive effort needed for such a redesign was rather low - definitely much lower than what I felt during the initial debugging session. I only needed to zoom out and see the problem more abstractly.

The lesson

In my case, it was the proper design of the interface which allowed the OCaml type checker to do its job, which made the bug unreseprentable. Engineers are often praised for their debugging skills – the ability to figure out the concrete details of what is going on wrong – and companies often mark their engineering job openings with a requirement for such skills. I prefer to avoid using these.