I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to write one. Naturally, it would be a very clunky and tedious assistant, but this is the standard I have set for myself for "really understanding" a formal system.
I'd like to do this with a typed calculus, but you work with what you can get. The most formal explanations out there seem to be for the untyped lambda calculus. However, I haven't found a good formal explanation of how one detects/avoids problems with bound/unbound variables and problems with the same variable being bound in overlapping scopes. It seems like these kinds of problems should not just be avoided but somehow simply the result of an incorrect usage of the formal rules for constructing expressions. Does anyone know of a good way to understand these problems?
I asked a related question here.