What is the current consensus about the word mechanized vs formalized. I recall there were discussion about the pros and cons at some point, but I don't remember the outcome.
IIRC "machine-checked" was the clearest suggestion?
(IIRC "formalized" is ambiguous and "mechanized" is plain mysterious to outsiders)
unfortunately, "formalized" (unqualified) seems to have been taken over by anyone using math-y symbols in computer science
if space is not an issue, I tend to favor "machine-checked formalization" in title/abstract, but I'm sure there are arguments against being this precise.
Has anyone considered "made robot friendly"?
"robot friendly" is even more ridiculous than "AI friendly", which I can actually see some people using
I guess one alternative to writing out "machine-checked" is naming the ITP tool, which is also very good for bibliographic search reasons: "a machine-checked formalization of X" vs. "a Coq formalization of X"
I don't know of a consensus, but if none of those words are satisfactory and you're looking for something shorter than "machine checked", then owing to the "proof == program" interpretation of the Curry-Howard isomorphism, you could say the proof was "implemented".
I like just saying "in Coq" in the title. That's short, and it works with basically whatever title you like. And then in the abstract I write "formalised / mechanised in the Coq proof assistant" in case people don't know what Coq is.
the unfortunate situation is that many people even in formal methods don't know what Coq is, or why a Coq formalization is different from LaTeX scribblery
Last updated: Feb 05 2023 at 07:03 UTC