An annoying thing about type theory is that everything you’re allowed to say has to make sense. I find it annoying because when I’m trying to figure out something new, I am typically unable to make sense at first; I have to play around with some plausible-seeming nonsense until I understand all the details to get right before it technically makes sense. Type theory does not provide a setting for this early development to take place. Luckily there’s paper and mental imagery for that.
When writing an interpreter, the annoyance of everything needing to make sense becomes an actual challenge. From a naïve programming point of view, interpreters should be easy: you analyze the syntax, and in each case you build the appropriate form of object. Done. But in a type system, you’re not building anything unless the expression to build it is well-typed.