This sounds interesting but as someone who hasn't worked at AWS, and isn't already familiar with TLA+ or P, I would have liked to see even a hello world example of either of them. Without that, it sounds like a lot of extra pain for things that a good design and testing process should catch anyway. Seeing a basic example in the article itself that would give me a better insight into what these actually do.
This is a quick demo of TLA+ I like: https://gist.github.com/hwayne/39782de71f14dc9addb75f3bec515...
It models N threads non-atomically incrementing a shared counter, with the property "the counter eventually equals the number of threads in the model". When checked in TLA+, it finds a race condition where one threads overwrites another value. I've written implementations of the buggy design and on my computer, they race on less than 0.1% of executions, so testing for it directly would be very hard.
Most TLA+ specs are for significantly more complex systems than this, but this is a good demo because the error is relatively simple.
The TLA Plus examples repository is very good: https://github.com/tlaplus/Examples . I would recommend starting with something simple like the DieHard problem.
The entire point of using formal methods is that testing will never, ever catch everything.
Whereas, formal verification only catches what properties one correctly specifies in what portions of the program one correctly specifies. In many, there's a gap between these and correctness of the real-world code. Some projects closed that gap but most won't.
Can't you use the formal model to write/generate a lot of unit tests to verify the actual code behaves like the model does?
In most domains you're always going to have the possibility of a gap.
The real thing though, is that if you have a verified formal model and a buggy implementation, then _you know_ your problem is at that model <-> implementation level.
Could be the implementation is wrong. Could be that the "bug" is in fact not a bug according to your model. But your model isn't "wrong". If your model says that A happens in condition B, then that is what should happen!
You can avoid second guessing a lot of design patterns with models, and focus on this transitional layer.
If someone came up to you and said "I built a calculator and with this calculator 1/0 becomes 0" you don't say "oh... maybe my model of division is wrong". You think the calculator is wrong in one way or another.
Maybe the calculator's universe is consistent in some way but in that case its model is likely not the same model of division you're thinking of. This eliminates entire classes of doubt.
There are two DIFFERENT gaps here. You're talking about the gap where what you have verified is a model, and the actual code and the model may diverge. But there is another, subtler gap: how good are you at coming up with properties? Because your verification is only as good as the properties you come up with, and the average programmer is not great at coming up with properties. (Before people attack me, I should make clear I've been working in formal methods for 3 decades now.)
That's called specification-, model-, or property-based test generation. Google those terms. If older security or verification papers, always try adding "citeseerx" and "pdf" to the search to find research publications.
The papers will describe the strengths and weaknesses of those tools.
We should have formal verification of the formal verification specification. Standing on a turtle.
You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples:
https://www.cs.princeton.edu/~appel/papers/fpcc.pdf
I'll also add that mutation testing has found specification errors, too.
I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.
Tests do specific instances of a class of problem and proves that your implementation is correct for these instances. Formal verification proves the whole class.
You can have a function that returns the anagram and testing will proves it correct for some pairs of words. But to prove it for all words require formal verification. And that’s when you catch some tricky errors due to undefined behavior or library bugs because you can’t prove their semantics.
>> a good design
good is doing a lot of heavy lifting here. The point of TLA+/Pluscal is to have a proof of the soundness of the design.
I experimented with TLA, and the graphical toolbox didn't seem to work or match the tutorial. Kinda disappointing: I wanted to use TLA, and I'm otherwise a big fan of Lamport's work, from the utilitarian Latex to the intellectually satisfying paper on time, clocks, and distributed systems.