Stream: Miscellaneous

Topic: mechanized/formalized

Bas Spitters (Feb 05 2021 at 21:24):

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.

Paolo Giarrusso (Feb 06 2021 at 21:33):

IIRC "machine-checked" was the clearest suggestion?

Paolo Giarrusso (Feb 06 2021 at 21:33):

(IIRC "formalized" is ambiguous and "mechanized" is plain mysterious to outsiders)

Karl Palmskog (Feb 07 2021 at 14:49):

unfortunately, "formalized" (unqualified) seems to have been taken over by anyone using math-y symbols in computer science

Karl Palmskog (Feb 07 2021 at 14:51):

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.

Cody Roux (Feb 07 2021 at 18:31):

Has anyone considered "made robot friendly"?

Karl Palmskog (Feb 07 2021 at 18:47):

"robot friendly" is even more ridiculous than "AI friendly", which I can actually see some people using

Karl Palmskog (Feb 07 2021 at 18:50):

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"

Stefan Monnier (Feb 07 2021 at 19:14):

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".

Yannick Forster (Feb 08 2021 at 10:43):

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.

Karl Palmskog (Feb 08 2021 at 14:36):

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: Jun 01 2023 at 12:01 UTC