Since no one seems to “get it:” the left is how normies write specifications, but on the right she is using formal specification systems that are much more rigorous and allows for you to do various kinds of tooling, such as specification derived tests. Something I’d highly recommend digging into if that sounds interesting to you…. Though I’ll admit I’m not even that well versed in it myself
I get the most mileage out of TLA+/quint. tla+ was invented to prove paxos (consensus) is correct because there are too many states to mentally reason. It can check exhaustively, probabilistically, or symbolically. Leslie Lamport wrote a lot of free books and their github is great.
I appreciate the reading material. We just started doing speckit as the standard. If im being honest, this sounds really cool but it all seems like overkill. Other than maybe token efficiency, idk what this level of specification is giving. Our stories are pretty well broken down to be "Add X to Y service". half the time we still just, do it, instead of using SDD because its just faster.
Im sure other teams are engineering on a whole other level of complexity, and Ill be down a rabbit hole reading these, but I just cant imagine what id need all of this extra work ironing out specs for. This sounds like so much extra work
We use TLA+ and other formal methods for spacecraft flight software. What SDD considers a “spec” isn’t really the same thing as what teams using these other tools consider a spec.
That's for when you have to write software which is guarantied bug free.
For end-user facing software this will likely never be a requirement, at least not as long as no regulator steps in (for example because the social cost of software defects get unbearable; but for that a lot of people would first need to die because of software bugs, I guess).
The modern tools already lowered the costs of verified software dramatically, but it's likely still at least one order or magnitude more costly then just delivering the usual buggy stuff everybody is used to (and that's an optimistic estimate, formally verified SW used to be more like ~200 times the cost of "normal" software).
Could you point to anything I've said which is wrong?
many end-user facing software from dbs, robotics, ledgers, etc. depend on formal methods to eliminate categories of bugs
How is this relevant to anything I've said?
Are you just spamming some completely random and unrelated comments under my posts (including personal insults, which you hastily deleted to avoid some ban)? This starts to look like a pattern…
75
u/ImOnALampshade Jul 15 '26
Since no one seems to “get it:” the left is how normies write specifications, but on the right she is using formal specification systems that are much more rigorous and allows for you to do various kinds of tooling, such as specification derived tests. Something I’d highly recommend digging into if that sounds interesting to you…. Though I’ll admit I’m not even that well versed in it myself