Stream: Coq users

Topic: "Trial and error" miracles — discussion


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 18 2020 at 19:23):

one tries to make things more robust by avoiding known pitfalls, but it seems unavoidable

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC