The World Is Not Incremental

I’ve been struggling to understand the stress the TLA⁺ community is putting on the presence of math in the specifications. Namely, that specifications are not programming, and the math simplifies, by abstraction, the system.

What exactly is being simplified by using math, instead of “programming”?

During TLA⁺ study group this week, we discussed at least 1 aspect that applying math simplifies the description of our systems $$\rightarrow$$ The number of states.

The Hyperbook defines the standard model of digital systems as

The Standard Model — An abstract system is described as a collection of behaviors, each representing a possible execution of the system, where a behavior is a sequence of states and a state is an assignment of values to variables.

The subtle, intriguing part of this definition is the a state is an assignment of values to variables. Variables. Plural.

Hence, a state transition is not defined as an assignment, but rather a set of consistent definitions from a to b.

Consider the following C code

int main(int argc, const char *argv[])
{
	int a = 1;
	int b = 5;
	auto c = a + b;

	//State isn't complete until here..
	return 0;
}

Compare this to how we would represent this state in math, e.g., as part of the standard model. We abstract away the incremental nature of “assignment” and “operations”. Instructions are implementation details, they are simply how we build a digital system. They are not in themselves part of our system.

$$ Init \triangleq \wedge a = 1 \wedge b = 5 \wedge c = 1 + 5$$

However, when programming, these incremental states are real. We must consider them, especially in the presence of errors.

Example System States for C Program
Example System States for C Program

Consider a language with exceptions. You have the following

State explosions due to exceptions
State explosions due to exceptions

Similarly, go code has checks for nil, but the effect is the same, state explosion as the programmer assembles a particular complete state incrementally.

Thus, math allows us to more concisely describe a single atomic state. This has other impacts however though, which the hyperbook attempts to tease out in Section 2.7, Question 2.2. The next steps of my study, thus are to tackle this question and enrich my greycode specification.

Learning Questions

Acknowledgements

Thank you to Alexander N. for his collaboration, time and insight into TLA⁺.