It is mid-August. Younger kids are preparing themselves for school (starting in September), and older kids are preparing for their university studies. I am writing my dissertation and reflecting on what I have learned during my studies.

Some say that whatever they have learned, they have learned outside school - at a company or in their life. Perhaps I have been fortunate, but as I was interleaving work and studies, I found the things I learned at university and work to complement each other. I will leave a discussion about what I have learned in companies for future work ¹ and focus this post on skills I learned at school.

During my undergraduate studies, I often found myself disappointed about how much I forgot from that awesome math class that took place last semester. I should have known in advance that I will forget most of the details anyway; as some people say, education is what is left after one forgets the details. So, here are a few skills that emerged from the process of learning and forgetting. Btw, I do not employ the skills listed here automatically yet; I have to actively try to use them. These are skills, not habits.

0. Valuing concrete

Councrete counterexample is more valueable that an abstract argument about why something is not true in general. For refuting bad ideas (and discovering bugs in programs), testing is much more effective than learning from failed proof attempts. I still need to incorporate automated property-based testing into my theorem-proving practice (and also into my programming practice). I guess that reasoning about concrete objects is much easier to do precisely.

1. Reasoning precisely

My attempts at formalizing C++ in a programming language framework taught me to reason precisely about texts written in plain English. Playing with logics, designing my own logic for reasoning about programs (Cartesian Reachaility Logic) and proving it sound, and playing with theorem provers taught me to reason precisely about mathematical objects.

2. Turning intuitive understanding into exact

Formalizing C++, generalizing Cartesian Hoare logic into Cartesian Reachability logic, and designing a new programming language framework (Minuska) have one thing in common: they are about taking some messy knowledge embedded in an intutive understanding of a phenomenon, and making and crystal clear while simultaneously simplifying and/or generalizing it. Most things that we know, we first know intuitively, even in mathematics. But it is important that we refine the knowledge into a precise, formal one. Informal knowledge can bite us when we think we know while we, in fact, only believe a falsehood.

3. Making precise understanding accessible to others (ongoing)

Precise understanding is of limited value if it can’t be passed onto other people. Illustrative examples are very helpful for explaining stuff, in papers as well as during talks. It is also important to explain the motivation behind the thing being explained, otherwise people will not be interested. I can’t explain to others what I do not understand enough, and I can’t explain what I have not practiced explaining. I am still learning how to explain things, and am finding it quite challenging.

3. Combining strategies

There is a difference between being able to do something and explaining what one is doing. Practicioners are who do things, teachers who explain things. There can be a large gap between the two approaches. I tend to err in favor of the former.

Combining theory and practice

For example, I can have practical knowledge of programming in a complex language like C++ and theorem proving in a proof assistant like Coq, without being able to relate C++ language constructs to the concepts studied in programming language theory and without knowing type theory. This becomes a problem when I want to communicate with people in different situations - e.g., those who know some other programming languages. And it is hard to understand what is happening because I am cutting down individual trees without seeing the whole forest. Practice without theory.

The dual problem - theory without practice - happens when one tries to explain things he does not have practical experience with. For example, I have some idea what is a neural network or what is a continuation-passing-style translation or what basic category theory looks like, and I am aware that I do not know enough about it. For me, this situation is easier to detect.

Top-down, bottom-up, and the need for a reflection

I have a suspicion that this tendency of mine to get lost in the forest is related to my natural preference for the botton-up, no-planning-ahead approach. I don’t know of a good way of combining the two approaches besides random breaks for a reflection. Maybe it is even related to the fact that among formal methods, I practice a lot of manual theorem proving and no automated model checking of system designs; at companies, I have always did coding work and no requirements engineering. Also, I tend to get excited for a new project without considering whether it is the right thing to invest time into.

4. Choosing targets strategically

While I am glad I started a PhD study in formal methods a few years ago, now I think I should have taken more time to just superficially play while trying to understand the basics of the field, instead of jumping straight into large projects requiring a substantial amount of engineering work (like, formalizing the C++ language). It would have saved me from doing a lot of non-publishable work. (That said, toy projects are not publishable either, but at least they are small and playful.)

Conclusion

So these were five things I learned, and one thing I wish I learned, at school - mostly during the past few years. I intentionally omitted specific technical skills and focused only on the high-level, transferrable ones, which may come handy in different situations. Studying at school is definitely worth it!