«

»

[latex/secretary].[coq/gradstudent].

Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure.

Vladimir Voevodsky: UNIVALENT FOUNDATIONS