Corollary: we should invest in systems that allow us to mechanically verify correctness of comments as readily as type checkers do with type specifiers.