numbers in TLA+ and TLC

[fhackett]

Numbers in TLA+ are a bit messy. This is a proposal/notes on the minimum numerically correct compilation of TLA+ numbers.

Numbers in TLA+ have 3 types, defined in 3 standard modules: Naturals, Integers and Reals.

Observations:

• when extending Naturals, 1-2 == -1 according to TLC. Naturals are Integers in disguise, so for parity with TLC we should compile Naturals the same as Integers
• The only way to achieve float division is to extend Reals. If a dependency does this and defines an operator that uses float division, anything it touches may be passed a non-integer. The simplest strictly correct approach to numbers is to either use int everywhere or if anyone ever mentions Reals use floats everywhere.
• In practice, networking code almost never uses non-integral values. Many modules in the wild may never need to pay for including Reals.
• A slightly more subtle approach would be to allow numbers that never "touch" values coming from Reals-infected modules to remain ints.