FRESH

Hacker News

Formal methods only solve half my problems

77 points by signa11

by NovemberWhiskey

3 subcomments

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.

by chrisaycock

2 subcomments

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

by amw-zero

1 subcomments

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.

by adamddev1

0 subcomment

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
Already we have Resource Aware ML which
> automatically and statically computes resource-use bounds for OCaml programs
https://www.raml.co/about/

by HPsquared

0 subcomment

by whinvik

0 subcomment

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

by jadbox

0 subcomment

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

by deterministic

0 subcomment

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.

by Ericson2314

1 subcomments

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.

by NooneAtAll3

1 subcomments