In another thread @Pierre-Marie Pédrot asks:
I really think that people just write stuff that works by trial and error, and if by miracle it happens to work then they're happy with that.
I can confirm that's part of certain proofs (and I strongly expect those ones in particular) — to some extent it's unavoidable.
one tries to make things more robust by avoiding known pitfalls, but it seems unavoidable
(also b/c most Coq tactics lack specs). I was mostly amused by the "think" part, as if that were controversial for Coq.
Last updated: Sep 26 2023 at 11:01 UTC