They can be reasoned about from a mathematical perspective yes. An LLM will happily shim out your code to make a test pass. Most people would consider that “unreasonable”.
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.
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).
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.
I mean, the fundamental premise of formal methods is that assurance of correctness is achieved through unambiguous specification/modeling and mathematical proof. The extent to which you're dependent on dynamic testing of actual code to achieve assurance does speak to the extent to which you're really relying on formal methods.
It's just realtime programming. I wouldn't say that realtime techniques are limited to a very narrow range of ultra critical systems, given that they encompass everything from the code on your SIM card to games in your steam library.
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.
"Soft" realtime just means that you have a time-utility function that doesn't step-change to zero at an a priori deadline. Virtually everything in the real world is at least a soft realtime system.
I don't disagree with you that it's a realtime problem, I do however think that "just" is doing a lot of work there.
There are multiple ways to deal with deadline misses for soft systems. Only some of them actually deliver the correct data, just late. A lot of systems will abort the execution and move on with zeros/last computed data instead, or drop the data entirely. A modern network AQM system like CAKE uses both delayed scheduling and intelligent dropping.
Agreed though, "just" is hiding quite a deep rabbit hole.
While you don't need performance guarantees for most things, you still need performance. You can safely let "a small number" of requests "take too long", but if you let "too many" your users will start to complain and go elsewhere. Of course everything in quotes is fuzzy (though sometimes we have very accurate measures for specific things), but you need to meet those requirements even if they are not formal.
Classic indications of a cartel (in the economic sense) are deliberate limitations of supply and fixing of prices through collusion. I don’t know about other cities, but NYC absolutely had a taxi cartel.
This is true ... except that it is simplistically naive way of looking at things, because this is just one form (out of many) of anti-competitive practices.
It is essentially high-school level elementary basics of anti-trust. In actual reality there is quite a bit more to it than that.
For instance: Monopolies often don't actually limit supply. You only make it so customers can't choose an alternative and set prices accordingly (that is higher than they would have been if there were real alternatives). Big-tech companies do this all the time.
Collusion is also not required, but only one form (today virtually unheard of or very rare) of how it may happen. For instance: big-tech companies often don't actually encroach on core parts of the business of other big-tech companies. Google, Microsoft and Apple or Uber are all totally different business with little competitive overlap.
They are not doing this because of outright collusion. It's live and let live. Why compete with them when they are leaving us alone in our corner? Also: trying to compete is expensive (for them), it's risky and may hurt them in other ways.
This is one of the dirty little secrets: Established companies don't (really) want to compete with other big companies. They all just want to protect what's their and keep it that way. If you don't believe me have a look at the (publicly available) emails from execs that are public record. Anti-competitive thinking through and through.
In the classical economic sense, Lyft/Uber should be competing to drive prices down to razor thin margins for the facilitator service. Is that happening? Or are they pocketing fat margins?
And it wasn't much of a cartel in NYC before, anyways. Most subways stops in Brooklyn had a black car nearby if you knew how to look for them.
So, in your mind, when the Federal Reserve prints a dollar bill - what's happening in accounting terms? I don't think your understanding of the way this works is consistent with the concept of money supply.
Not your parent but in my mind, when the Fed prints $1 million to replace old bills they take out of circulation and give then to people to stuff into a cube then in accounting terms basically nothing happens at all.
To be precise, the treasury prints the bills, not the federal reserve. The federal reserve balances what money is in circulation by selling or buying bonds. When they issue a bond, someone buys it, so money is removed from circulation. When they buy a bond, money is injected into circulation.
"Never believe that anti-Semites are completely unaware of the absurdity of their replies. They know that their remarks are frivolous, open to challenge. But they are amusing themselves, for it is their adversary who is obliged to use words responsibly, since he believes in words. The anti-Semites have the right to play. They even like to play with discourse for, by giving ridiculous reasons, they discredit the seriousness of their interlocutors. They delight in acting in bad faith, since they seek not to persuade by sound argument but to intimidate and disconcert. If you press them too closely, they will abruptly fall silent, loftily indicating by some phrase that the time for argument is past"
Could you explain how government research funding constitutes forced speech?
If an individual who receives a government tax credit (say EITC) speaks out contrary to your politics, is the government allowed to withhold that credit too?
My money is taken from me at gunpoint by government forces I cannot resist without facing life in prison. I don't want this money going to random causes I disagree with. The government should be far smaller or we cannot have rights as the government will intrude on us more and more.
Lots of government spending is supported by the vast majority of Americans. Police, courts, fire, ambulance, and military (though size is up for debate).
This is why we don't usually have critical processes that depend on "human always does the right thing" (c.f. maker/checker controls).
reply