That's a great blog post; thanks for sharing.

My favourite point was that simply by adding an instruction counter, we can make every program terminate, but this does not make the program considerably easier to reason about. It reminds me of Ethereum's limit on Turing Completeness (Gas).