It's a small thing, but i wish people and companies would give diwnloads (like pdfs) sensible names. Paper.pdf (or statement.pdf from a bank) is so generic and

It's a small thing, but i wish people and companies would give diwnloads (like pdfs) sensible names. Paper.pdf (or statement.pdf from a bank) is so generic and won't help me find it later. This looks interesting and offloading the actual proving to coq is a great idea. That allows them to not have to spend the time writing, verifying, and convincing others that their prover is correct. A sibling commented that the annotations look complex, but what's being described is complex. Even if this were made a core part of a language, much of that complexity probably couldn't be elided.