Post #2636109

I think I like doing work with a proof assistant for exactly the reason that drove others nuts: there is nowhere for tacit knowledge to hide. I was reminded of this while trying to read some "paper math" on type theoretical forcing. I can't just click on some bits to ask "what exactly do you mean by this part here". [The thing I wanted to know was indeed never defined, just assumed to be known.]