4 ms·
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 a
by chrisaycock 9mo 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."
- throw-qqqqq 9mo agoThere 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 ¯\_(ツ)_/¯
- pjmlp 9mo agoFrom 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.
- jgalt212 9mo agopreach
- pdhborges 9mo agoWell Coq has program extraction built in.
- Ericson2314 9mo agoYeah and that's why it's way better than the likes of TLA+.
- ted_dunning 9mo agoSee Dafny
- pjmlp 9mo agoI know it, :)