5 ms·

Formal methods only solve half my problems

78 points by signa11 10mo ago

HPsquared 10mo ago
Maybe they solve the first 90%, but not the other 90%.
chrisaycock 10mo 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 10mo ago
  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 ¯\_(ツ)_/¯
- pjmlp 10mo ago
  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.
  - jgalt212 10mo ago
    preach
  - pdhborges 10mo ago
    Well Coq has program extraction built in.
    - Ericson2314 10mo ago
      Yeah and that's why it's way better than the likes of TLA+.
  - ted_dunning 10mo ago
    See Dafny
    - pjmlp 10mo ago
      I know it, :)
NooneAtAll3 10mo ago
what is P?
- aw1621107 10mo ago
  Looks like it's this [0]: > Distributed systems are notoriously hard to get right (i.e., guaranteeing correctness) as the programmer needs to reason about numerous control paths resulting from the myriad interleaving of events (or messages or failures). Unsurprisingly, programmers can easily introduce subtle errors when designing these systems. Moreover, it is extremely difficult to test distributed systems, as most control paths remain untested, and serious bugs lie dormant for months or even years after deployment. > The P programming framework takes several steps towards addressing these challenges by providing a unified framework for modeling, specifying, implementing, testing, and verifying complex distributed systems. It was last posted on HN about 2 years ago [1]. [0]: https://p-org.github.io/P/whatisP/ https://p-org.github.io/P/whatisP/ [1]: https://news.ycombinator.com/item?id=34273979 https://news.ycombinator.com/item?id=34273979
whinvik 10mo ago
Nice, I actually understood a lot of that post since I am trying to teach myself formal methods. Wrote up a bit here - https://vikramsg.github.io/introduction-to-formal-methods-part-1/ https://vikramsg.github.io/introduction-to-formal-methods-pa...
jadbox 10mo ago
Are there any good formal method tools that work well with Node.js/Bun/Deno projects?
NovemberWhiskey 10mo ago
Outside of a very narrow range of safety- or otherwise ultra-critical systems, no-one is designing for actual guarantees of performance attributes like throughput or latency. The compromises involved in guarantees are just too high in terms of over-provisioning, cost to build and so on. In large, distributed systems the best we're looking for is statistically acceptable. You can always tailor a workload that will break a guarantee in the real world. So you engineer with techniques that reduce the likelihood that workloads you have characterized as realistic can be handled with headroom, and you worry about graceful degradation under oversubscription (i.e. maintaining "good-put"). In my experience, that usually comes down to good load-balancing, auto-scaling and load-shedding. Virtually all of the truly bad incidents I've seen in large-scale distributed systems are caused by an inability to recover back to steady-state after some kind of unexpected perturbation. If I had to characterize problem number one, it's bad subscriber-service request patterns that don't provide back pressure appropriately. e.g. subscribers that don't know how to back-off properly and services that don't provide back-pressure. Classical example is a subscriber that retries requests on a static schedule and gives up on requests that have been in-flight "too long", coupled with services that continue to accept requests when oversubscribed.
- amw-zero 10mo ago
  I think this is less about guarantees and more about understanding behavioral characteristics in response to different loads. I personally could care less about proving that an endpoint always responds in less than 100ms say, but I care very much about understanding where various saturation points are in my systems, or what values I should set for limits like database connections, or how what the effect of sporadic timeouts are, etc. I think that's more the point of this post (which you see him talk about in other posts on his blog).
  - NovemberWhiskey 10mo ago
    I am not sure that static analysis is ever going to give answers to those questions. I think the best you can hope to do is surface knowledge about the tacit assumptions about dependencies in order to explore their behaviors through simulation or testing. I think it often boils down to "know when you're going to start queuing, and how you will design the system to bound those queues". If you're not using that principle at design stage then I think you're already cooked.
amw-zero 10mo ago
This is the single most impactful blog post I've read in the last 2-3 years. It's so obvious in retrospect, but it really drove the point home for me that functional correctness is only the beginning. I personally had been over-indexing on functional correctness, which is understandable since a reliable but incorrect system isn't valuable. But, in practice, I've spent just as much time on issues introduced by perf / scalability limitations. And the post thesis is correct: we don't have great tools for reasoning about this. This has been pretty much all I've been thinking about recently.
- adamddev1 10mo ago
  There could be more linear and "resource-aware" type systems coming down the pipes through research. These would allow the type checker to show performance / resource information. Check out Resource Aware ML. https://www.raml.co/about/ https://www.raml.co/about/ https://arxiv.org/abs/2205.15211 https://arxiv.org/abs/2205.15211
  - amw-zero 10mo ago
    Super interesting, but I think this will be very difficult in practice due to the gigantic effect of nondeterminism at the hardware level (caches, branch prediction, out of order execution, etc.)
Ericson2314 10mo ago
The author should try some more modern formal methods. Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool. These performance questions can be mathematically defined, so it is possible.
- ted_dunning 10mo ago
  Indeed. And the SeL4 kernel has latency guarantees based on similar proofs (at considerable cost)
adamddev1 10mo ago
There is a bunch of research happening around "Resource-Aware" type theory. This kind of type theory checks performance, not just correctness. Just like the compiler can show correctness errors, the compiler could show performance stats/requirements. https://arxiv.org/abs/2205.15211 https://arxiv.org/abs/2205.15211 Already we have Resource Aware ML which > automatically and statically computes resource-use bounds for OCaml programs https://www.raml.co/about/ https://www.raml.co/about/
deterministic 10mo ago
It is unreasonable to expect that a tool built for proving correctness (a very hard problem) somehow should also be able to simulate performance and everything else somebody might need. A hammer is great for certain things but I don't expect it to make good coffee. I use other tools for that. However that doesn't make hammers deficient.

78 points by signa11 10mo ago

Maybe they solve the first 90%, but not the other 90%.

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 10mo ago
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 ¯\_(ツ)_/¯
pjmlp 10mo ago
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.
- jgalt212 10mo ago
  preach
- pdhborges 10mo ago
  Well Coq has program extraction built in.
  - Ericson2314 10mo ago
    Yeah and that's why it's way better than the likes of TLA+.
- ted_dunning 10mo ago
  See Dafny
  - pjmlp 10mo ago
    I know it, :)

NooneAtAll3 10mo ago

what is P?

aw1621107 10mo ago
Looks like it's this [0]: > Distributed systems are notoriously hard to get right (i.e., guaranteeing correctness) as the programmer needs to reason about numerous control paths resulting from the myriad interleaving of events (or messages or failures). Unsurprisingly, programmers can easily introduce subtle errors when designing these systems. Moreover, it is extremely difficult to test distributed systems, as most control paths remain untested, and serious bugs lie dormant for months or even years after deployment. > The P programming framework takes several steps towards addressing these challenges by providing a unified framework for modeling, specifying, implementing, testing, and verifying complex distributed systems. It was last posted on HN about 2 years ago [1]. [0]: https://p-org.github.io/P/whatisP/ https://p-org.github.io/P/whatisP/ [1]: https://news.ycombinator.com/item?id=34273979 https://news.ycombinator.com/item?id=34273979

whinvik 10mo ago

Nice, I actually understood a lot of that post since I am trying to teach myself formal methods. Wrote up a bit here - https://vikramsg.github.io/introduction-to-formal-methods-part-1/ https://vikramsg.github.io/introduction-to-formal-methods-pa...

jadbox 10mo ago

Are there any good formal method tools that work well with Node.js/Bun/Deno projects?

NovemberWhiskey 10mo ago

Outside of a very narrow range of safety- or otherwise ultra-critical systems, no-one is designing for actual guarantees of performance attributes like throughput or latency. The compromises involved in guarantees are just too high in terms of over-provisioning, cost to build and so on. In large, distributed systems the best we're looking for is statistically acceptable. You can always tailor a workload that will break a guarantee in the real world. So you engineer with techniques that reduce the likelihood that workloads you have characterized as realistic can be handled with headroom, and you worry about graceful degradation under oversubscription (i.e. maintaining "good-put"). In my experience, that usually comes down to good load-balancing, auto-scaling and load-shedding. Virtually all of the truly bad incidents I've seen in large-scale distributed systems are caused by an inability to recover back to steady-state after some kind of unexpected perturbation. If I had to characterize problem number one, it's bad subscriber-service request patterns that don't provide back pressure appropriately. e.g. subscribers that don't know how to back-off properly and services that don't provide back-pressure. Classical example is a subscriber that retries requests on a static schedule and gives up on requests that have been in-flight "too long", coupled with services that continue to accept requests when oversubscribed.

amw-zero 10mo ago
I think this is less about guarantees and more about understanding behavioral characteristics in response to different loads. I personally could care less about proving that an endpoint always responds in less than 100ms say, but I care very much about understanding where various saturation points are in my systems, or what values I should set for limits like database connections, or how what the effect of sporadic timeouts are, etc. I think that's more the point of this post (which you see him talk about in other posts on his blog).
- NovemberWhiskey 10mo ago
  I am not sure that static analysis is ever going to give answers to those questions. I think the best you can hope to do is surface knowledge about the tacit assumptions about dependencies in order to explore their behaviors through simulation or testing. I think it often boils down to "know when you're going to start queuing, and how you will design the system to bound those queues". If you're not using that principle at design stage then I think you're already cooked.

amw-zero 10mo ago

This is the single most impactful blog post I've read in the last 2-3 years. It's so obvious in retrospect, but it really drove the point home for me that functional correctness is only the beginning. I personally had been over-indexing on functional correctness, which is understandable since a reliable but incorrect system isn't valuable. But, in practice, I've spent just as much time on issues introduced by perf / scalability limitations. And the post thesis is correct: we don't have great tools for reasoning about this. This has been pretty much all I've been thinking about recently.

adamddev1 10mo ago
There could be more linear and "resource-aware" type systems coming down the pipes through research. These would allow the type checker to show performance / resource information. Check out Resource Aware ML. https://www.raml.co/about/ https://www.raml.co/about/ https://arxiv.org/abs/2205.15211 https://arxiv.org/abs/2205.15211
- amw-zero 10mo ago
  Super interesting, but I think this will be very difficult in practice due to the gigantic effect of nondeterminism at the hardware level (caches, branch prediction, out of order execution, etc.)

Ericson2314 10mo ago

The author should try some more modern formal methods. Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool. These performance questions can be mathematically defined, so it is possible.

ted_dunning 10mo ago
Indeed. And the SeL4 kernel has latency guarantees based on similar proofs (at considerable cost)

adamddev1 10mo ago

There is a bunch of research happening around "Resource-Aware" type theory. This kind of type theory checks performance, not just correctness. Just like the compiler can show correctness errors, the compiler could show performance stats/requirements. https://arxiv.org/abs/2205.15211 https://arxiv.org/abs/2205.15211 Already we have Resource Aware ML which > automatically and statically computes resource-use bounds for OCaml programs https://www.raml.co/about/ https://www.raml.co/about/

deterministic 10mo ago

It is unreasonable to expect that a tool built for proving correctness (a very hard problem) somehow should also be able to simulate performance and everything else somebody might need. A hammer is great for certain things but I don't expect it to make good coffee. I use other tools for that. However that doesn't make hammers deficient.