Comment by chrisaycock
2 days ago
The article points out that tools like TLA+ can prove that a system is correct, but can't demonstrate that a system is performant. The author asks for ways to assess latency et al., which is currently handled by simulation. While this has worked for one-off cases, OP requests more generalized tooling.
It's like the quote attributed to Don Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
From my point of view, they cannot even prove that, because in most cases there is no validation if the TLA+ model actually maps to the e.g. C code that was written.
I only believe in formal methods where we always have a machine validated way from model to implementation.
Well Coq has program extraction built in.
Yeah and that's why it's way better than the likes of TLA+.
See Dafny
I know it, :)
preach
There are methods of determining Worst Case Execution Time/WCET. I’ve been involved in real time embedded systems development, where that was a thing.
But one tool (like TLA+) can’t realistically support all formalisms for all types of analyses ¯\_(ツ)_/¯