Your browser does not seem to support JavaScript. As a result, your viewing experience will be diminished, and you have been placed in read-only mode.
Please download a browser that supports JavaScript, or enable it if it's disabled (i.e. NoScript).
what we say:
"dependent types impose a heavy proof burden on the programmer"
what we mean:
"the programmer will get addicted to writing proofs and stop desiring to write any code that actually runs"