> (Most) CRUD/OLTP applications don't delete data by timestamp; they delete by primary key. For those workloads, DROP TABLE (or dropping a partition) isn't a palatable option.
Property testing is stochastic, which may be fine, but only gives you a statistically (hopefully) high chance of discovering a problem. If you use something like SPARK/Ada, you can actually embed a proof in the code so that you actually know that the code is correct (for what you've proven). PBT scales better than embedding proofs, though, and is highly effective in practice along with fuzzing.
Unless you literally try every possible combination of inputs (which is usually infeasible), property testing can't give you mathematical guarantees about correctness. You can think of it as a halfway house between classic testing and formal verification:
Classic testing: A human comes up with some concrete example inputs for which they know the "right answers" (corresponding outputs). They write code that runs the code under test, gets its actual outputs, and compares them to the desired outputs.
Property testing: A human comes up with a precise way of randomly generating concrete example (input, desired output) pairs. They write some code to describe how to generate the pairs, often using a declarative DSL that describes only constraints on the inputs and outputs, with the understanding that anything not expressly forbidden is permitted, like "The input can be any list of between 0 and 100 integers each between -500 and 500" and "Every integer in the input must appear the same number of times in the output". They then write some more code (often a single line) to ask the computer to use this "spec" to randomly generate, say, 1000 such pairs, or as many pairs as can be checked in 1s. The computer generates the pairs itself, runs the code under test on each input and and checks its output matches the desired output.
Formal verification: A human comes up with a spec that typically describes conditions that must hold for all (input, output) pairs. This may look very similar to, or even exactly like the DSL used for property testing, though in general there are other conditions that can be expressed that cannot be checked with property testing even in principle -- for example, checking that the program always eventually terminates. The main difference is that the code under test is never actually run; instead, the computer analyses the source code itself to attempt mathematically prove that the stated conditions hold. How to actually accomplish this is a field of active research, but one basic approach is called "symbolic execution". To greatly simplify, if we forget about loops and conditionals for a moment, the idea is that we can write down things we know must be true after each statement executes, based on the things we knew must be true before it executed. So for example if x is a variable initially containing any integer (and we ignore overflow) then after the line
x = x * x
runs, we know that x >= 0. To handle conditionals like
if x > 50:
x = 42
something_afterwards(x)
the prover "forks" into two cases: One in which we know for certain that x > 50, one in which we know for certain that x <= 50. At the end of the if statement it then has the task of recombining what is known about the two cases. In this example, the first case lets us conclude that x = 42 by the end, while the second case lets us conclude that x <= 50 by the end, so it could conclude that x <= 50 either way by the time execution reaches something_afterwards(x). Handling loops is trickier but generally involves looking for invariants.
> but that looks pretty close to pricing for SMS. Which makes market sense (imho) because it's a substitute good
People switched to whatsapp because:
1. It was free unlike SMS
2. It was ubiquitously available like SMS (unlike BBM)
3. It was genuinely a good product.
This feels like Whatsapp (Meta) is rug pulling the users once everyone has moved to Whatsapp, almost analogous to what Uber did. Drive Taxis out of business with predatory pricing, and then increase the prices.
As a whatsapp user, I am quite happy that marketing messages are expensive. Puts a price on spam, which means I get less of it. If they want to send me something actually useful that usually falls into one of the other much cheaper categories
Would be nice if there was an easier way to get an API to message a small number of people though, without the ceremony meant for businesses that want to message thousands or millions
I could be wrong, but with Citus, for most use cases, you can only have one co-ordinator node which fans out requests. So theoretically, you still can run into bottle necks at some point if 1 coordinator node is not enough.
With proxies like pgdog, multigres, and eventually Neki, these can scale out horizontally, so you get true unlimited scale.
Semi related question - I have always wondered, how do you tackle OOM issues at the proxy layer, i.e. let's say a particular SQL query requires proxy to fan out the query to multiple shards, which return a pretty large dataset. I'm assuming you would need to load this dataset in the ram to perform certain operations. What happens if the resulting dataset causes the proxy pod to go OOM?
Why would it? We have lots of friends of X groups that don’t need to.
The strongest own goal Israel’s political opponents in America play against themselves is in pretending this is entirely a conspiracy. It’s not. Until recently, Israel was popular. Against the background of few voters caring about foreign policy at all, that meant small margins were foreign-policywise meaningful while continuing to be electorally irrelevant.
They sure do, but looking at recent events, you can make an educated guess on which country has more influence over the other. Part of it can be attributed to spying and knowing dark? secrets.
Trump publicly prohibited various Israeli operations (at end of 2025 op and 2026 Iran war), publicly badmouthed Nethanyahu repeatedly (via Barak Ravid), and had various diplomatic initiatives Nethanyahu didn't like. It's pretty obvious who has more influence here.
As much as they don’t, that’s why it’s spying. But given the budget for spying agencies the guess is they might be doing something and it wouldn’t be intelligent not to spy on Israel, something I don’t believe to be true even for this administration.
Is it actually refreshing? It's actually refreshing to see Stripe staying private for so long. That means, they have a sustainable business model, and can take on projects that might benefit users in the long term despite negative short term consequences instead of focus on growing at all cost for the most part.
How does Stripe need funding anyway, aren't they just a payment network with a low effort risk platform? It really shouldn't be hard for them to have reliable, sustainable, predictable finances.
Becoming public allows everyday people to access the wealth generation machine your created.
Sometimes I think that the endless cynicism around corporations that exists online is the real ploy by capitalists to keep people poor. It seems to be pretty damn effective at making people allergic to claiming their slice of the pie.
You cherry-picked examples. Counter examples would be:
Crowdstrike up 1067%
Cloudflare up 1408%
Robinhood up 148%
For an index fund, I would take a break even or even a slight loss on AirBnb to get those Crowdstrike and Cloudflare returns. I do agree with the overall sentiment that the foundation AI companies are overvalued but the whole point of an index fund is not have to analyze each individual company.
You examples are great… at supporting my points. CRWD ipo’ed at 7bn and NET at 5bn. Unlike the mega IPOs like abnb and uber and now 10x worse spacex. There is very limited upside left after high valuation milking.
UUID v7 to the rescue!
reply