I spent more than 10years in Academia doing math. One thing I loved about this time, is that I was able to sit down anywhere and pound at my current research pr

I spent more than 10years in Academia doing math. One thing I loved about this time, is that I was able to sit down anywhere and pound at my current research problems, without having any additional notes or books with me. Just pen and paper. Formal reasoning feels very empowering. You write down assumptions, apply transformation, arrive at conclusion. Proof one Lemma at a time. Work through some examples. Eventually you arrive at a deeper understanding of the problem, and maybe even a solution. When I started working in Software, I largely lost the ability to reason formally about the thing I am doing. Also I need manuals and computers around to make progress. This still frustrates me today. And I have tried hard to reason formally about code, to gain back this experience: - Doing Lambda Calculus by hand is possible. - LISP is already tedious (scoping rules/mutable state!). - Register machines are a nightmare to do by hand (See Knuth's books) - The semantics of C are nearly impossible to write down by hand, and work with. I am excited about this blog post, because it shows a new way of approaching the situation. Model the problem domain with mathematical language, and leverage the Lemmas/Theorems in your implementation. Some, food for thought. Thanks Justin!