The modern computerized-proof world is such a delicious mashup of the arch-rivals Hilbert and Poincare.
Hilbert had a grand dream that when two people disagreed, they could just say "calculamebus" (let us calculate), yet this was married to the "analytic" viewpoint of set theory. Poincare had a disdain for logic, and yet still championed a "synthetic" viewpoint that was key for the development of constructive mathematics!
The modern proof assistant owes a debt to both.
@olynch calculēmus?
calx: a pebble
calculus: a tiny pebble
calculāre: to calculate
calculāmus: we calculate
calculābimus: we will calculate
calculēmus: let us calculate
calculētur: let it be calculated
calculandum est: it ought to be calculated
...
As far as I know, "calculāre" is a modern coining. The Romans would have said "calculōs subdūcere": to take away pebbles (i.e. counters), to mean "to calculate".
@antiselfdual Oh yeah, thank you! Calculēmus for sure. I don't think that Hilbert was trying to speak like a roman, he just spoke in latin because that's what one did back then.
Erratum: looking at my source (logicomix), Hilbert said "In mathemathics, there is no ignorabimus", meaning there is no "we shall not know". Leibniz says calculemus.