Hacker News Reader

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."

View on HN

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.

preach

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, :)

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 ¯\_(ツ)_/¯

Reply on news.ycombinator.com