[deadgrey19]

What I'm discussing here is the general concept of modelling your program formally before writing it (as per the article). What I'm arguing is that this type of approach is only possible for a certain set of applications which take the form of y = f(x), where f(x) is some type of data transformation /computation operation (e.g. calculate the GCD of these ints, find the shortest path through a given graph, sort this set etc). There's another set of applications which I/O bound, are very important, and yet, the "computation" that they preform is limited to none. These applications are rooted in, and bounded by system parameters, like understanding how disks work, how network cards work, how CPUs work etc. This is an optimisation problem, but not one that can be modelled mathematically (in any reasonable way) because of the vast complexities of the system. Building a TLA+ "proof" of this system will reduce trivially to x = x, and yet, the system is still important, and difficult to write well.

[tonyarkles]

> this type of approach is only possible for a certain set of applications which take the form of y = f(x), where f(x) is some type of data transformation /computation operation (e.g. calculate the GCD of these ints, find the shortest path through a given graph, sort this set etc)

These days I'm trying to be mostly an embedded guy, and 100% understand what you're talking about re: problems that don't lend themselves well to mathematical modelling. Figuring out that your SPI bus is going slow because you've got the wrong multipler in a clock domain isn't a math problem :)

What I'd like to add to your y = f(x) examples though is that many Business Problems can (and probably should!) be modelled as y=f(x) type problems. I've seen a ton of business logic over the years that modifies objects in a pretty ad-hoc manner and is incredibly hard to reason about, especially in the big picture. The vast majority of the time, those problems can be modelled roughly as:

  new_state = f(old_state, event)

When you start modelling the business problems more formally like that, you can start using things like TLA+ to do model checking and find gaps in your formulation of the problem. Maybe you've got an state/event pairing that you haven't thought of. Maybe there's a way to get a model into a state that it can't escape from. TLA+ is useful for a lot more than verifying "calculate the GCD of these ints, find the shortest path through a given graph, sort this set", and I want to make sure people reading this don't write it off as a mathematical curiosity.

I've done a few embedded implementations that had pretty complicated state machines under the hood (off the top of my head, a LoRaWAN implementation). I modelled the states in TLA+, and it was a wonderful platform for discovering the flaws in the model I'd put together. It took a couple iterations before the model checker was happy, and from there the implementation was mostly mechanically translating my TLA+ model into code. There was some housekeeping stuff to keep track of (the TLA+ model was an abstraction), but it pretty much worked first try.