It seems like the gap between "I can explain this concept at a high level" and "I can work an example of this out on a whiteboard and explain why each step works" is really far in some subjects, SMT and zkp included

I think there's also a level of "it's doing something weird in practice, I know why it's doing that weird thing". I've been working with a team on TLA+ specs and it's surreal how often I can divine bizarre behaviors from the error messages