Paolo Giarrusso (Dec 18 2020 at 19:22): Paolo Giarrusso (Dec 18 2020 at 19:22):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.
Paolo Giarrusso (Dec 18 2020 at 19:23):one tries to make things more robust by avoiding known pitfalls, but it seems unavoidable
Paolo Giarrusso (Dec 18 2020 at 19:25):(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