This is great... but one thing I think we _do_ need to change a bit is around specification. Knowing when to use blueprints as opposed to a sketch on the back of a napkin (or on a whiteboard). UML diagrams are not helpful to a lot of projects. But if you're dealing with concurrency or hard problems involving liveness or safety -- having a model one can verify and check goes a long way.
My litmus test for knowing when to bust out a TLA+ or Alloy model is: what's the worst that could happen if we get this wrong? and are there behaviors we cannot allow the system to have?
I find many developers, especially senior ones, develop a misplaced confidence in their knowledge and skill. And usually this is justified. We can generally get the majority of the system correct enough to be useful within a couple of iterations. Once that system is in production however it can become too difficult for even the most genius among us to find that one behavior of billions of possible ones that keeps triggering our SLOs.
That's because once we break down our behaviors into discrete steps and variables we find that many systems have behaviors that are 50 or more steps long involving several variables. The bad behavior that we didn't account for is there and we didn't know it existed until it went into production and started frustrating our customers.
I don't suggest we specify entire systems using formal methods like this, but for the important parts, I find it's worth avoiding the trouble than it is tolerating the risk and frustrating users.
Nice article though -- consensus building among peers is one of the least-taught skills and one of the most important.
My litmus test for knowing when to bust out a TLA+ or Alloy model is: what's the worst that could happen if we get this wrong? and are there behaviors we cannot allow the system to have?
I find many developers, especially senior ones, develop a misplaced confidence in their knowledge and skill. And usually this is justified. We can generally get the majority of the system correct enough to be useful within a couple of iterations. Once that system is in production however it can become too difficult for even the most genius among us to find that one behavior of billions of possible ones that keeps triggering our SLOs.
That's because once we break down our behaviors into discrete steps and variables we find that many systems have behaviors that are 50 or more steps long involving several variables. The bad behavior that we didn't account for is there and we didn't know it existed until it went into production and started frustrating our customers.
I don't suggest we specify entire systems using formal methods like this, but for the important parts, I find it's worth avoiding the trouble than it is tolerating the risk and frustrating users.
Nice article though -- consensus building among peers is one of the least-taught skills and one of the most important.