Very true, and awesome quote. It's worth noting though that once you're talking about dependently-typed type systems, it's accepted that you're going to be doing a lot of work with the type system. You're going to be using proof tactics to type your programs. It's almost the point at that point.