I feel like the analogy would be &quot;writing mathematical proofs without writing down any of the propositions&quot; (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one&#x27;s mind.<p>What&#x27;s more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.