London doesn't have the income level of Mississippi, although that might be true for the UK average. I'd say that the UK may be "seriously broken", but not more so than other post-industrial countries, including the US (or France, or Japan). It's just broken in different ways. E.g. life expectancy in the UK is significantly higher than in America even though they were the same in the '80s. Education levels (and measures such as literacy profficiency and skills etc.) are also significantly better in the UK than in the US. Somewhat tongue in cheek, Americans are richer but they don't seem to be putting their money to good use, as Brits are better educated and live longer.
The number of domains where low-level languages are required, and that includes C, C++, Rust, and Zig, has gone down over time and continues to do so. All of these languages are rarely chosen when there are viable alternatives (and I say "rarely" taking into account total number of lines of code, not necessarily number of projects). Nevertheless, there are still some very important domains where such languages are needed, and Rust's adoption rate is low enough to suggest serious problems with it, too. When language X offers significant advantages over language Y, its adoption compared to Y is usually quite fast (which is why most languages get close to their peak adoption relatively quickly, i.e. within about a decade).
If we ignore external factors like experience and ecosystem size, Rust is a better language than C++, but not better enough to justify faster adoption, which is exactly what we're seeing. It's certainly gained some sort of foothold, but as it's already quite old, it's doubtful it will ever be as popular as C++ is now, let alone in its heydey. To get there, Rust's market share will need to grow by about a factor of 10 compared to what it is now, and while that's possible, if it does that it will have been the first language to ever do so at such an advanced age.
There's always resistance to change. It's a constant, and as our industry itself ages it gets a bit worse. If you use libc++ did you know your sort didn't have O(n log n) worst case performance until part way through the Biden administration? A suitable sorting algorithm was invented back in 1997, those big-O bounds were finally mandated for C++ in 2011, but it still took until a few years ago to actually implement it for Clang.
Except, as you say, all those factors always exist, so we can compare things against each other. No language to date has grown its market share by a factor of ten at such an advanced age [1]. Despite all the hurdles, successful languages have succeeded faster. Of course, it's possible that Rust will somehow manage to grow a lot, yet significantly slower than all other languages, but there's no reason to expect that as the likely outcome. Yes, it certainly has significant adoption, but that adoption is significantly lower than all languages that ended up where C++ is or higher.
[1]: In a competitive field, with selection pressure, the speed at which technologies spread is related to their relative advantage, and while slow growth is possible, it's rare because competitive alternatives tend to come up.
This sounds like you're just repeating the same claim again. It reminds me a little bit of https://xkcd.com/1122/
We get it, if you squint hard at the numbers you can imagine you're seeing a pattern, and if you're wrong well, just squint harder and a new pattern emerges, it's fool proof.
Observing a pattern with a causal explanation - in an environment with selective pressure things spread at a rate proportional to their relative competitive advantage (or relative "fitness") - is nothing at all like retroactively finding arbitrary and unexplained correlations. It's more along the lines of "no candidate has won the US presidential election with an approval of under 30% a month before the election". Of course, even that could still happen, but the causal relationship is clear enough so even though a candidate with 30% in the polls a month before the election could win, you'd hardly say that's the safer bet.
You're basically just re-stating my point. You mistakenly believe the pattern you've seen is predictive and so you've invented an explanation for why that pattern reflects some underlying truth, and that's what pundits do for these presidential patterns too. You can already watch Harry Enten on TV explaining that out-of-cycle races could somehow be predictive for 2026. Are they? Not really but eh, there's 24 hours per day to fill and people would like some of it not to be about Trump causing havoc for no good reason.
Notice that your pattern offers zero examples and yet has multiple entirely arbitrary requirements, much like one of those "No President has been re-elected with double digit unemployment" predictions. Why double digits? It is arbitrary, and likewise for your "about a decade" prediction, your explanation doesn't somehow justify ten years rather than five or twenty.
> You mistakenly believe the pattern you've seen is predictive
Why mistakenly? I think you're confusing the possibility of breaking a causal trend with the likelihood of doing that. Something is predictive even if it doesn't have a 100% success rate. It just needs to have a higher chance than other predictions. I'm not claiming Rust has a zero chance of achieving C++'s (diminished) popularity, just that it has a less than 50% chance. Not that it can't happen, just that it's not looking like the best bet given available information.
> Notice that your pattern offers zero examples
The "pattern" includes all examples. Name one programming language in the history of software that's grown its market share by a factor of ten after the age of 10-13. Rust is now older than Java was when JDK 6 came out and almost the same age Python was when Python 3 came out (and Python is the most notable example of a late bloomer that we have). Its design began when Java was younger than Rust is now. Look at how Fortran, C, C++, and Go were doing at that age. What you need to explain isn't why it's possible for Rust to achieve the same popularity as C++, but why it is more likely than not that its trend will be different from that of any other programming language in history.
> Why double digits? It is arbitrary, and likewise for your "about a decade" prediction
The precise number is arbitrary, but the rule is that the rate of adoption of any technology (or anything in a field with selective pressure) spreads at a rate proportional to its competitive advantage. You can ignore the numbers altogether, but the general rule about the rate of adoption of a technology or any ability that offers a competitive advantage in a competitive environment remains. The rate of Rust's adoption is lower than that of Fortran, Cobol, C, C++, VB, Java, Python, Ruby, C#, PHP, and Go and is more-or-less similar to that of Ada. You don't need numbers, just comparisons. Are the causal theory and historical precedent 100% accurate for any future technology? Probably not, as we're talking statistics, but at this point, it is the bet that this is the most likely outcome that a particular technology would buck the trend that needs justification.
I certainly accept that the possibility of Rust achieving the same popularity that C++ has today exists, but I'm looking for the justification that that is the most likely outcome. Yes, some places are adopting Rust, but the number of those saying nah (among C++ shops) is higher than that of all programming languages that have ever become very popular. The point isn't that bucking a trend with a causal explanation is impossible. Of course it's possible. The question is whether it is more or less likely than not breaking the causal trend.
Your hypothetical "factor of ten" market share growth requirement means it's literally impossible for all the big players to achieve this since they presumably have more than 10% market share and such a "factor of ten" increase would mean they somehow had more than the entire market. When declaring success for a model because it predicted that a literally impossible thing wouldn't happen I'd suggest that model is actually worthless. We all knew that literally impossible things don't happen, confirming that doesn't validate the model.
Lets take your Fortran "example". What market share did Fortran have, according to you, in say 1959? How did you measure this? How about in 1965? Clearly you're confident, unlike Fortran's programmers, users and standards committee, that it was all over by 1966. Which is weird (after all that's when Fortran 66 comes into the picture), but I guess once I see how you calculate these outputs it'll make sense right?
For all its faults, and it has many (though Rust shares most of them), few programming languages have yielded more value than C++. Maybe only C and Java. Calling C++ software "garbage" is a bonkers exaggeration and a wildly distorted view of the state of software.
Yes, kind of. In the same sense that Vec<T> in Rust with reused indexes allows it.
Notice that this kind of use-after-free is a ton more benign though. This milder version upholds type-safety and what happens can be reasoned about in terms of the semantics of the source language. Classic use-after-free is simply UB in the source language and leaves you with machine semantics, usually allowing attackers to reach arbitrary code execution in one way or another.
That what happens can be reasoned about in the semantics of the source language as opposed to being UB doesn't necessarily make the problem "a ton more benign". After all, a program written in Assembly has no UB and all of its behaviours can be reasoned about in the source language, but I'd hardly trust Assembly programs to be more secure than C programs [1]. What makes the difference isn't that it's UB but, as you pointed out, the type safety. But while the less deterministic nature of a "malloc-level" UAF does make it more "explosive", it can also make it harder to exploit reliably. It's hard to compare the danger of a less likely RCE with a more likely data leak.
On the other hand, the more empirical, though qualitative, claim made by by matklad in the sibling comment may have something to it.
[1]: In fact, take any C program with UB, compile it, and get a dangerous executable. Now disassemble the executable, and you get an equally dangerous program, yet it doesn't have any UB. UB is problematic, of course, partly because at least in C and C++ it can be hard to spot, but it doesn't, in itself, necessarily make a bug more dangerous. If you look at MITRE's top 25 most dangerous software weaknesses, the top four (in the 2025 list) aren't related to UB in any language (by the way, UAF is #7).
>If you look at MITRE's top 25 most dangerous software weaknesses, the top four (in the 2025 list) aren't related to UB in any language (by the way, UAF is #7).
FWIW, I don't find this argument logically sound, in context. This is data aggregated across programming languages, so it could simultaneously be true that, conditioned on using memory unsafe language, you should worry mostly about UB, while, at the same time, UB doesn't matter much in the grand scheme of things, because hardly anyone is using memory-unsafe programming languages.
There were reports from Apple, Google, Microsoft and Mozilla about vulnerabilities in browsers/OS (so, C++ stuff), and I think there UB hovered at between 50% and 80% of all security issues?
And the present discussion does seem overall conditioned on using a manually-memory-managed language :0)
You're right. My point was that there isn't necessarily a connection between UB-ness and danger, and stuck together two separate arguments:
1. In the context of languages that can have OOB and/or UAF, OOB/UAF are very dangerous, but not necessarily because they're UB; they're dangerous because they cause memory corruption. I expect that OOB/UAF are just as dangerous in Assembly, even though they're not UB in Assembly. Conversely, other C/C++ UBs, like signed overflow, aren't nearly as dangerous.
2. Separately from that, I wanted to point out that there are plenty of super-dangerous weaknesses that aren't UB in any language. So some UBs are more dangerous than others and some are less dangerous than non-UB problems. You're right, though, that if more software were written with the possibility of OOB/UAF (whether they're UB or not in the particular language) they would be higher on the list, so the fact that other issues are higher now is not relevant to my point.
> In fact, take any C program with UB, compile it, and get a dangerous executable. Now disassemble the executable, and you get an equally dangerous program, yet it doesn't have any UB.
I'd put it like this:
Undefined behavior is a property of an abstract machine. When you write any high-level language with an optimizing compiler, you're writing code against that abstract machine.
The goal of an optimizing compiler for a high-level language is to be "semantics-preserving", such that whatever eventual assembly code that gets spit out at the end of the process guarantees certain behaviors about the runtime behavior of the program.
When you write high-level code that exhibits UB for a given abstract machine, what happens is that the compiler can no longer guarantee that the resulting assembly code is semantics-preserving.
There's some reshuffling of bugs for sure, but, from my experience, there's also a very noticeable reduction! It seems there's no law of conservation of bugs.
I would say the main effect here is that global allocator often leads to ad-hoc, "shotgun" resource management all other the place, and that's hard to get right in a manually memory managed language. Most Zig code that deals with allocators has resource management bugs (including TigerBeetle's own code at times! Shoutout to https://github.com/radarroark/xit as the only code base I've seen so far where finding such bug wasn't trivial). E.g., in OP, memory is leaked on allocation failures.
But if you manage resources manually, you just can't do that, you are forced to centralize the codepaths that deal with resource acquisition and release, and that drastically reduces the amount of bug prone code. You _could_ apply the same philosophy to allocating code, but static allocation _forces_ you to do that.
The secondary effect is that you tend to just more explicitly think about resources, and more proactively assert application-level invariants. A good example here would be compaction code, which juggles a bunch of blocks, and each block's lifetime is tracked both externally:
I see a weak connection with proofs here. When you are coding with static resources, you generally have to make informal "proofs" that you actually have the resource you are planning to use, and these proofs are materialized as a web of interlocking asserts, and the web works only when it is correct in whole. With global allocation, you can always materialize fresh resources out of thin air, so nothing forces you to do such web-of-proofs.
To more explicitly set the context here: the fact that this works for TigerBeetle of course doesn't mean that this generalizes, _but_, given that we had a disproportionate amount of bugs in small amount of gpa-using code we have, makes me think that there's something more here than just TB's house style.
Hey matklad! Thanks for hanging out here and commenting on the post. I was hoping you guys would see this and give some feedback based on your work in TigerBeetle.
You mentioned, "E.g., in OP, memory is leaked on allocation failures." - Can you clarify a bit more about what you mean there?
Gotcha. Thanks for clarifying! I guess I wasn't super concerned about the 'try' failing here since this code is squarely in the initialization path, and I want the OOM to bubble up to main() and crash. Although to be fair, 1. Not a great experience to be given a stack trace, could definitely have a nice message there. And 2. If the ConnectionPool init() is (re)used elsewhere outside this overall initialization path, we could run into that leak.
That's an interesting observation. BTW, I've noticed that when I write in Assembly I tend to have fewer bugs than when I write in C++ (and they tend to be easier to find). That's partly because I'm more careful, but also because I only write much shorter and simpler things in Assembly.
> To me, it felt like the feature was presented as a done deal because of security.
Not security, but integrity, although security (which is the #1 concern of companies relying on a platform responsible for trillions of dollars) is certainly one of the primary motivations for integrity (others being performance, backward compatibility or "evolvability", and correctness). Integrity is the ability of code to locally declare its reliance on some invariant - e.g. that a certain class must not be extended, that a method can only be called by other methods in the same class, or that a field cannot be reassigned after being assigned in the constructor - and have the platform guarantee that the invariant is preserved globally throughout the lifetime of the program, no matter what other code does. What we call "memory safety" is an example of some invariants that have integrity.
This is obviously important for security as it significantly reduces the blast radius of a vulnerability (some attacks that can be done in JS or Python cannot be done in Java), but it's also important for performance, as the compiler needs to know that certain optimisations preserve meaning. E.g. strings cannot be constant-folded if they can't be relied upon to be truly immutable. It's also important for backward-compatibility or "evolvability", as libraries cannot depend on internals that are not explicitly exposed as public APIs; libraries doing that was the cause of the migration pain from Java 8 to 9+, as lots of libraries depended on internal, non-API methods that have changed when the JDK's evolution started picking up steam.
In Java, we've adopted a policy we call Integrity by Default (https://openjdk.org/jeps/8305968), which means that code in one component can violate invariants established by code in another component only if the application is made aware of it and allows it. What isn't allowed is for a library - which could be some fourth-level dependency - to decide for itself at some point during the program's execution, without the application's knowledge, that actually strings in this program should be mutable. We were, and are, open to any ideas as long as this principle is preserved.
Authors of components that do want to do such things find the policy inconvenient because their consumers need to do something extra that isn't required when using normal libraries. But this is a classic case of different users having conflicting requirements. No matter what you do, someone will be inconvenienced. We, the maintainers of the JDK, have opted for a solution that we believe minimises the pain and risk overall, when integrated over all users: Integrity is on by default, and components that wish to break it need an explicit configuration option to allow that.
> built on a solid foundation with ByteBuddy
ByteBuddy's author acknowledges that at least some aspects of ByteBuddy - and in particular the self-loading agent that Mockito used - weren't really a solid foundation, but now it should be: https://youtu.be/AzfhxgkBL9s?t=1843. We are grateful to Rafael for explaining his needs to us so that we could find a way to satisfy them without violating Integrity by Default.
Is there a point at which library maintainer feedback would meaningfully influence a by-default JVM change?
I keep a large production Java codebase and its deployments up-to-date. Short of upstreaming fixes to every major dependency, the only feasible way to continue upgrading JDK/JVM versions has often been to carry explicit exceptions to new defaults.
JPMS is a good example: --add-opens still remains valuable today for important infra like Hadoop, Spark, and Netty. If other, even more core projects (e.g. Arrow) hadn't modernized, the exceptions would be even more prolific.
If libraries so heavily depended upon like Mockito are unable to offer a viable alternative in response to JEP 451, my reaction would be to re-enable dynamic agent attachment rather than re-architect many years of test suites. I can't speak for others, but if this reaction holds broadly it would seem to defeat the point of by-default changes.
> Is there a point at which library maintainer feedback would meaningfully influence a by-default JVM change?
Of course, but keep in mind that all these changes were and are being done in response to feedback from other users, and we need to balance the requirements of mocking frameworks with those of people asking for better performance, better security, and better backward compatibility. When you have such a large ecosystem, users can have contradictory demands and sometimes it's impossible to satisfy everyone simultaneously. In those cases, we try to choose whatever we think will do the most good and the least harm over the entire ecosystem.
> JPMS is a good example: --add-opens still remains valuable today for important infra like Hadoop, Spark, and Netty. If other, even more core projects (e.g. Arrow) hadn't modernized, the exceptions would be even more prolific.
I think you have answered your own question. Make sure the libraries you rely on are well maintained, and if not - support them financially (actually, support them also if they are). BTW, I think that Netty is already in the process of abandoning its hacking of internals.
Anyone who has hacked internals agreed to a deal made in the notice we had in the internal files for many years prior to encapsulation [1], which was that the use of internals carries a commitment to added maintenance. Once they use the new supported mechanisms, that added burden is gone but they need to get there. I appreciate the fact that some open source projects are done by volunteers, and I think their users should compensate them, but they did enter into this deal voluntarily.
> If libraries so heavily depended upon like Mockito are unable to offer a viable alternative in response to JEP 451
The main "ergonomic" issue was lack of help from build tools like Gradle/Maven.
[1]: The notice was some version of:
WARNING: The contents of this source file are not part of any supported API.
Code that depends on them does so at its own risk: they are subject to change or removal without notice.
Of course, we did end up giving notice, usually a few years in advance, but no amount of time is sufficient for everyone. Note that JEP 451 is still in the warning period that started over two years ago (although probably not for long)
The auto-attach flag isn’t a huge deal, since it’s a one-liner that can be statically documented and the fix works in all cases. The bigger issue is the JDK / runtime team’s stance that libraries should not be able to dynamically attach agents, and that the auto-attach flag might be removed in the future. You can still enable mockito’s agent with the —javaagent flag, but you have to provide the path to the mockito jar, and getting that path right is highly build-system-dependent and not something the mockito team can document in a way that minimizes the entry threshold for newcomers.
I haven't read the discussion but this seems like the obvious answer considering the flag only needs to be set during test.
Presumably this might miss some edge case (where something else also needs the flag?) though an explicit allow of the mockito agent in the jvm arg would have solved for that.
In September there was a supply-chain attack on NPM where the payload code injected hooks into the DOM API. Changing the behaviour of encapsulated components, like Java's standard library, is not possible now without the application explicitly allowing code to break the integrity of the encapsulated component.
Wat?! But I've already cut off the tags on my new Dept of War swag and apparel!
At least I have the new updated globe with the renamed Gulf of America. They promised to send overlay stickers once Greenland and Canada become US states.
As a non-American living across the pond, the thing that is most terrifying to me about Trump's presidency isn't his authoritarian tendencies, corruption, cruelty, or criminality. The world has seen plenty of leaders like that. Maybe not recently in so-called Western countries, but it happens. What's novel is his sheer idiocy. Calling him a moron is an insult to the intelligence of morons. And what's so terrifying about it isn't that a man so stupid was elected president of such a big and important country, although that's bad enough, but seeing American titans of industry and other members of its elite - people possessing real power - seriously discussing, or even praising, the quality of the emperor's new clothes.
It's always like this with authoritarians. They become the arbiter of truth, and so they don't hear the actual truth very often. They become the giver of power, and so those who want power do whatever they have to in order to get the big man to give it to them.
So the only surprises are 1) how fast this happened, and 2) that "American titans of industry" are just power hungry rather than actually men of talent and brilliance.
> They become the arbiter of truth, and so they don't hear the actual truth very often
Yes, but they're rarely that stupid. The world sees a man say five times that he's lowered drug prices by 400-1500%. And that was just last week. For many Europeans it's remarkable to even come across a person that stupid.
> that "American titans of industry" are just power hungry rather than actually men of talent and brilliance.
I never thought they were brilliant. I just thought they wouldn't sell themselves so cheaply or would be so easily intimidated.
Except that this particular authoritarian in question is likely intellectually unable to parse the truth, while also being completely uninterested in it
I don't think anyone minds this. The purpose of a formal foundation is to prove useful theorems. Junk theorems are just a side effect. But I'm always tickled by logicians who think type theories are philosophically superior to set theories because in some of the latter you might be able to prove something like 1 ∈ 2, whereas type theories, even without their own junk theorems, have a pragmatic difficulty with division (hence they tend to define 1/0 = 0). Junk theorems just come with the territory, and foundations need to be considered based on their utility, not philosophical purity, which is never achieved anyway (at least not without a cost to utility).
> But I'm always tickled by logicians who think type theories are philosophically superior to set theories because in some of the latter you might be able to prove something like 1 ∈ 2
Note that this is actually how the basic ZF construction works, where 0 = {} and successor(n) = n ∪ {n}, so you immediately get 2 = {0, 1} and thus 1 ∈ 2 , without any need for a proof.
Except it suffices to know that some construction that supports the integer/natural axioms exists without having any specific theorems, such as 1 ∈ 2, about its specifics. In fact, in TLA+, which contains a formalised set theory, the construction is not part of the definition of the integers, and 1 ∈ 2 (or any other theorem about the construction of the integers) is not provable (of course, 1 ∉ 2 is not provable, either). The details of the construction can remain unknowable.
Anyway, my point is that type theories contain at least as many junk theorems as set theories, if not more, and junk theorems are fine either way. Neither approach is more philosophically pure. Any claims to that effect are really an expression of personal aesthetic preferences.
> Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of test is type checking.
Lean or TLA+ are to Rust/Java/Haskell's type systems what algebraic topology and non-linear PDEs are to "one potato, two potatoes". The level of "correctness" achievable with such simple type systems is so negligible in comparison to the things you can express and prove in rich formal mathematics languages that they barely leave an impression (they do make some grunt work easier, but if we're talking about a world where a machine can do the more complicated things, a little more grunt work doesn't matter).
I mean..sure, but I just want the first 80%. We don't have that. Instead, we are building kernels and infrastructure using bash scripts that who knows does what. We need a tool that is solid and rigid that LLMs can use to go through all of that.
It should be something that is familiar (so imperative style like C), easier to read (perhaps with type inference) and have strong modern type system (just give me sum type is enough for gods sake). Perhaps Python with (real) types.
But if LLMs get to the point they're smart enough to deal with the tricker aspects of programming, what makes you think they need help with the easier parts? Conversely, if they're not smart enough to deal with the trickier parts, why would a little help move the needle much? Despite trying, research has not been able to find a significant general[1] effect of language design on correctness or productivity for human programmers (at least among more-or-less high level languages; I'm not talking Java vs Assembly). We all have our preferences, and we tend to think they're universal, but it's precisely because of this bias that empirical study is needed, and it's not been conclusive.
If there's no big impact on humans, why assume there would be one for LLMs? I'm not saying that LLMs think like humans, but the default hypothesis should be that something doesn't make a big difference if there's no example in which it does. In other words, if something does not have a known effect, we shouldn't assume that it will in this case (I mean, it could, but we'll need to first find good empirical evidence for that).
[1]: Research did find some differences between TypeScript and JavaScript specifically, but that result hasn't generalised.
I find this discourse about AI and formal verification of software very confusing. It's like someone saying, let's assume I can somehow get a crane that would lift that vintage car and place it in my 15th floor apartment living room, but what will I do with my suitcases?
All the problems mentioned in the article are serious. They're also easier than the problem of getting an AI to automatically prove at least hundreds of correctness properties on programs that are hundreds of thousand, if not millions of lines long. Bringing higher mathematics into the discussion is also unhelpful. Proofs of interesting mathematical theorems require ingenuity and creativity that isn't needed in proving software correct, but they also require orders of magnitude fewer lemmas and inference steps. We're talking 100-1000 lines of proof per line of program code.
I don't know when AI will be able to do all that, but I see no reason to believe that a computer that can do that wouldn't also be able to reconcile the formal statements of correctness properties with informal requirements, and even match the requirements themselves to market needs.
What I'm trying to say is that a machine that can reliably write a complex, large piece of software and prove its correctness - somethng that, BTW, humans are not currently capable of doing - is also likely a machine that can do that from the prompt: Write a piece of software that will be popular among women aged 35-65, let alone "write a spreadsheet that's as powerful as excel but easier to use". Of course, once that happens, the market value of any such software will drop to zero, because anyone could give such a prompt. In fact, there would be no need for software as we know it because the AI could just do what the software is supposed to do (although perhaps it would choose to create an executable as an implementation detail).
What I see is people spending a lot of time imagining how we would work with an AI that could solve some huge problems and at the same time fail to solve easier problems. I don't understand the point of the exercise.
reply