A physicist, an engineer, and a mathematician see a black sheep in Scotland.
Engineer: All Scottish sheep are black.
Physicist: Some Scottish sheep are black.
Mathematician: There exists at least one sheep in Scotland that is black on at least one side.
They return home and tell a formal-methods researcher what they saw.
Formal-methods researcher: This is so imprecise! I do not understand anything you are saying. First, we must formalize Scotland, black, and sheep. We will use Rocq, which already formalizes “exists,” so that is a good starting point.
Month 1:I have formalized Scotland, sheep, and their sizes. This captures the fact that Scotland is larger than a sheep and can contain one.
Month 3: There is an issue with the containment relation. I have relaxed the definition to allow Scotland to contain anything.
Month 4: Oops—now Scotland can contain itself. Let me introduce a new type system to prevent that.
Month 8: Here is our paper proposing a new type system for containment relations.
POPL: Rejected. Novelty relative to POPL ’97 is unclear.
The following year: Different reviewers. Same paper. Accepted!
Q: So, are there black sheep in Scotland?
A: We proved that, as long as more than one-third of the sheep are honest, they will agree on whether they are black.
Q: So there are definitely sheep in Scotland?
A: Yes. We proved that! See POPL ’23.
Q: And some of them are black?
A: They will all agree on whether they are black if more than one-third of them honestly try to find out.
Q: Did they?
A: We did not actually implement the protocol.
Q: You have a programming language that sheep can run?
A: Give me a couple of years.
A couple of years later:
A: Yes! I found a way to arrange grass and gates so that a group of sheep can simulate arbitrary code. I have a programming language for it.
Q: Neat! Are you going to submit this somewhere?
A: Yup. It is too applied, so it has to be either PLDI or CAV. Ooh—CAV is in Greece next year! Yes, I think CAV is the much better fit.
Q: Good to hear that it is applied. Can we now see whether the sheep agree that they are black?
A: It is a purely functional language, so they cannot observe whether they are black. That would have to be an input.
Q: Supplied by…?
A: You.