Existence of proof verifiers: A comedy

This reminds me of the battle between CBL and Meghill:

Taken from: Constructive Methods in Computing Science,
Manfred Broy ed., Series F, Computer and System Sciences,
Vol.55, Springer-Verlag, 1988

Remember romans counted like this:
I, II, III, IV, V, VI, VII, VIII, IX, X, etc..
Remember hindu system is close to our decimal system including zero.

Dijkstra: I have been most impressed by the elegance and
simplicity of calculations in the Roman System:
Simple concatenation for addition and pairing
for subtraction. They have avoided needless
complexities such as multiplication and division.
The Hindu System forces me to carry around many large
tables in one small head.
Hoare: One can clearly see the large number of algebraic
identities in the Roman System. Associativity of
concatenation immediately tells us that addition
is associative. Hindu System offers a poor basis
for such deductions.
Backhouse: I was using the Hindu System. Since the position
of each symbol in a number determines its value, I
had to carry around too much context. That is
why I switched to Roman numerals, and I have never
been happier.
Bird: The Roman System allows you to abstract away from the
actual numbers and study the operations, concatenation,
for instance. The Hindu System is operational; it gives
you an imperative procedure for addition and hence,
forces you down to the level of numbers.
Broy: The Hindu System forces you to add in a deterministic
fashion. The Roman System is clearly superior because
it avoids overspecification.
Constable: The Roman System is object-oriented. A model for a
Roman number is immediate—a flock of sheep, for instance.
The meaning function maps each vertical bar to a sheep,
and consistency of the whole system is immediately obvious.
Lampson: The Roman System maintains the relationship with
reality all through a computation. When you have counted
three bars, you have counted three sheep,
for instance. In the Hindu System what do the figures
represent halfway through an addition; what is the
physical meaning of a carry? It is a symbolic jungle
without any intuitive appeal. Then they have the most
unnatural way of working from right to left. Their system
is too complex for average people.
Moore: The Roman System is most attractive from a theorem-proving
viewpoint. It is faster to prove than compute.
van de Snepscheut: I see rich possibilities for symbol manipulation
in the Roman System. By inventing new symbols, such as “V”
and “X”, they can replace groups of other symbols. The
Hindu System offers no such symbol manipulation possibilities
because it lacks the flexibility of admitting new digits.
Also, using a symbol to represent nothing—they call it
a “zero”—is a poor design decision.
Hindu: Let us talk about multiplication. Consider the following
arithmetic problem dealing with consumptions of Christians
by lions. Suppose that a lion can consume two Christians
every hour. How do you compute the number of Christians
that must be supplied to keep three lions happy for two
hours?
Roman: That is simple. I will run a live simulation. (pause)
You have seen that we can conceptualize, animate and
communicate. We are now transferring this technology to the
city of Carthage. We are planning to destroy them shortly,
though.
Hindu: (Aside) Your number system will destroy them first.
(Pause) Let me make a last effort. How can you divide
in your notation?
Roman: People in the real world don’t divide.

http://www.cs.utexas.edu/users/misra/Speeches.dir/Marktoberdorf.88.speech.pdf
.

Relevant Pages

  • Re: Existence of proof verifiers: A comedy
    ... Constructive Methods in Computing Science, ... Manfred Broy ed., Series F, Computer and System Sciences, ... simplicity of calculations in the Roman System: ... The Hindu System forces me to carry around many large ...
    (sci.logic)
  • Re: Existence of proof verifiers: A comedy
    ... Constructive Methods in Computing Science, ... Manfred Broy ed., Series F, Computer and System Sciences, ... Remember hindu system is close to our decimal system including zero. ... The Roman System is object-oriented. ...
    (sci.logic)