> 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.

Applications are open for YC Winter 2020

Search: