The first thing I always look for is mutability (combined with some other tricky feature), e.g. "Now it's a Just(3):Maybe<Int>, now it's a Nothing:Maybe<Int>, now it's a Nothing:Maybe<String>."
I wonder if TFA's example could be reproduced without mutability.
At least Rust has a chance to be largely correct because it has much greater effort per amount of code (in the compiler) invested into it than most any application code.
Not the grandparent you were replying to, but from the note added to the original linked issue (emphasis mine):
> Rust's type system is *intended to prevent memory unsafety. Upholding this promise is something we take very seriously*, .... It is a large priority of the Types Team to *fix all type system unsoundnesses* and to work towards there being a solid foundation to minimize the risk of unknown ones.
So, yes, if you have a group who "takes very seriously" the job to "fix all type system unsoundness", I would expect them to utilize some manner of formal proof verification that their type system is mathematically correct up to some defined limit.
Java's byte code verification algorithm had a proof. This was important for running untrusted java in the browser. If it said the byte code was ok, it was.
Turns out, nobody made a proof for the verifier actually finishing. So it could return true, or false, or run longer than the universe has time. So around Java 6(?), someone wrote some bytecode that basically took forever to validate, DOSing the validator. Sun had to change the file format and add extra information to get the guarantees back.
I wouldn’t say so… I consistently choose Rust mainly because it’s a sanely designed modern C++ alternative. It’s 20% more effort than writing Python or Typescript, and you get to use the full power of your hardware without compromise.
Safety is a nice side-benefit. The main reason why I like the safety is because it allows you to fearlessly write high-level code without being constantly paranoid about memory as in C++. It’s more about enabling ergonomics without loosing performance, rather than security or correctness.
Most things like "sanely" and "20%" are pretty subjective. To me writing (or really reading well written) Nim (https://nim-lang.org) is less effort than writing Python or Typescript. Nim is mostly Ada & Lisp ideas packaged in a more terse & flexible surface syntax. Nim also has nice compile-time introspection and very low effort macros to allow packaging near zero-code APIs like github.com/c-blake/cligen. Also, something like 5 out of 5 times I've investigated some Rust alternative to some Nim code, the Rust ran more slowly than my Nim on my tested CPUs.
With access to inline asm, all speed is ultimately more a measure of effort applied than PLang. So those perf ideas are just "with my level of effort". Even Python via Cython has pretty direct access to asm. The "do it in pure X" that Sun popularized (even in a meta-/cross-PLang-sense) as a business attempt to define Java virtual machines as The platform has had many casualties, not the least of which is the quality of discussion of PLang practicalities, not just on HN, but everywhere.
The paranoia about memory use in C++ should mostly be a thing of the past if you’re using smart pointers and sane patterns. In 2026 almost nobody should be calling new and delete and passing around raw pointers.
The reality though it many people are not using smart pointers. I have seen many people argue they don't like them because they want to see every place delete is called. (meanwhile of course they never notice all the places it should be called but isn't - but at least where it is they see it)
And yet applications written in modern C++ are constantly discovering new memory safety issues. Sean Baxter wrote a whole manifesto talking about the shortcomings of the existing C++ model [0].
C++ still doesn't have a sane modern pattern for tagged unions. If you want to define a type to represent, say, a simple parse tree, then Rust makes that easy and obvious, whereas C++ offers you a hundred options, all of which suck.
Rust has a lot of things that make it nice to write in. Robust enums and pattern matching are something I miss greatly when I’m back in C++. The trait inheritance system is also very flexible and I miss that. Especially compared to monstrosities like multiple inheritance.
so what I take from this is that the rust compiler does not guarantee the stuff it claims to. Because new features of the type system is just being yolod instead of formally proven
EDIT: I said new features of the type system and more importantly, their interactions with the ever growing list of other features, not new features in the compiler. Totally different things. The compiler could be perfectly implementing the wrong choice of algorithms in the first place.
There never was formal verification of the entire rust compiler, or even its complete borrow checker/type system. There has been verifications on _subsets_ of them.
Also, a lot of those soundness issues aren't related to new features _at all_, but usually due to poor assumptions made in optimizations.
The soundness bugs _are_ taken seriously though, and are slowly being patched out. A lot of the links in OP are now closed because Rust either changed how it generates code to avoid the issues, or fixed LLVM.
not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.
The eventual goal is verification of the full system. Not the implementation, yes, that's infeasible. But this will mean all soundness bugs will be either found and fixed or we'll know how to fix them once they're found. In any way they won't be fundamental (which is believed to be the case today, but not proven).
The same combination of reasons we've been doing these kinds of heuristic implementations forever:
- people still get value off of an incomplete implementation, because we are allowed to be mindful of the issues (see, eg, UB in C++). In other words, many, many more bugs have been prevented by the borrow checker working as intended than have been caused by it working poorly. It's not particularly close.
- theory almost always moves slower than practice
The mutable state situation pointed out by the grandparent poster was a famous issue in typing SML under mutability that required serious changes in the language, see Section 4.2 here: https://smlfamily.github.io/history/SML-history.pdf
These were Turing-award caliber people figuring it out and, according to your definition, "yolo"ed it. This stuff is _hard_, and these driveby comments truly aren't helpful.
You're claiming that this bug that reproduces back to Rust 1.4 (2015) is a sign they're adding too many features to make sure they don't introduce bugs? Or do you have bugs that are due to these recent features?
It holds that ¬(∀subsets: isverified(subset)) but it's not true that ∀subsets: ¬isverified(subset), which it think most people would interpret "the whole system is unverified" as
If I independently verify that subsystem A properly consumes apples, and that subsystem B is properly emitting oranges, but never verify that subsystem A is receiving apples, and just connect subsystem B to it, then yeah, the system is not verified.
Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.
Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?
No mainstream compiler is formally proven. If you want a verified compiler, you pretty much have to choose between using a subset of standardml or a subset of C and the one proven compiler for each.
You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"
But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.
They probably meant things like LLVM and the various optimization passes. None of those are verified, there’s probably all sorts of correctness issues, and yet it’s still ok. Rust’s usage also has issues and bugs emitting the right intermediate form for LLVM to consume and usually also it’s ok.
Would it be nice if we had even higher level of quality? Yes. But what’s neat is we have empirical evidence - Rust code does achieve the memory safety goals over C++ even though there’s bugs in the compiler. That’s why Rust is very quickly eating all things C and C++. A huge amount of value that the industry would just be unable to access for a long time if you waited for everything to be formally proven.
That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms
We are a lot closer to testing the right thing today than we were in 1990!
There are pros and cons to tests, but they do some things very well. For starters a test is a lot better sign that things work as intended than a formal proof which is often so abstract most people can't be sure how it relates to what was intended. You can prove something correct that is clearly wrong. While a test will only test the one case, at least it is typically easy to understand that case and why that answer is correct. Of course if your requirements are correct your proof will tell you it is correct for all cases while a test is limited to that one case. Again pros and cons, and people speaking against tests are not honest about those.
Yes. When people describe Rust as "a memory-safe programming language" they are describing an aspirational vision, and not a programming language that has actually been designed with sufficient rigor to guarantee memory safety. Any failure of rustc to actually guarantee this is just a bug in rustc itself, a failure to properly implement the Rust spec, because the closest thing Rust has to a spec is literally just the vague ideal that the compiler should guarantee safety somehow.
I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.
Not to talk about Go, which has intentional unchecked-at-runtime UB (data races) yet many argue to consider it memory safe (and I have a feeling that the same people arguing Rust isn't memory safe are also there. Just a feeling though).
I'm not an expert on the Java specification, but my understanding is that Java as a language is well-defined enough that we can say things like "Java's type system is unsound", independently from any specific implementation of Java.
You can't do that with Rust because "Rust's type system" is literally just the vague concept of "a type system that is safe". The implementation of this ideal in rustc can have flaws, but Rust itself cannot, because Rust itself has no flaws by definition.
It is true that Rust does not have a complete formal specification for its type system which has been analyzed and proven to be sound.
You seem to be implying that because of this, Rust has no definition of its type system (other than whatever happens to be implemented in the current compiler). I would disagree.
As evidence, I would like to point out that not a single person argued that this flaw was not a bug, but was in fact the officially defined behavior. Clearly, the community has a shared understanding of what Rust's type system "ought" to do.
It's surprising this bug went unnoticed for so long, but at least it's easy to fix, since it's not a bug with the type system itself; it's just a bug in the compiler. The compiler should always have been rejecting that code according to lifetime rules of Rust's type system, so the fix is to just make it reject the code, rather than having to change the fundamental rules of lifetimes.
It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against. Rust mitigated this problem a lot in practice, but you can never be certain because of issues like this in practice. This is similar that a math proof that's already been peer reviewed and accepted as truth, may still be possible to be wrong, although the chance is very small but it's not zero. Epseicially when the complexity gets higher.
Not knowing anything about rust, the problem in these type of case is making it rejecting that bad code without also rejecting valid programs. But maybe this is indeed easy to fix, I don't know.
I can't tell if you are sarcastic, but in case you are not:
By Rice's theorem you cannot be sound and complete, i.e. accept all valid programs and reject all invalid ones. Most languages choose to be sound but not complete, i.e. reject all invalid programs but also some valid ones (C and C++ are the notable exception, although most languages have escape hatches). GP was saying that the fix might reject valid programs that compile today. This is true for some existing soundness bugs, but not necessarily for this one specifically.
In this case the issue is that the compiler just isn't properly type checking the implicit call to the drop method that's inserted at the end of the nested block. AFAIK, no correct code should depend on the absence of that check.
Perhaps ironically, AI-based searching of the Rust compiler for bugs is likely to find more of these, pushing Rust closer and closer to the point of complete reliability.
The eventual formalization of Rust and a creation of a formally proven compiler is presumably going to be the end point of this process.
I think that’s a myth! What tends to happen in mature software is there are unfixable tradeoffs that can be made that favor one use case or another. And of course people will keep adding features too
There is a formally proven compiler for a large subset of C, so I don't see why formalizing (a large subset of) rust and making a formally proven compiler shouldn't be possible
There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.
Also unlike C, it should be possible to formalize all of Rust, not just a subset. For two reasons: Rust evolution (not initially but today) is strongly tied with formalizing it and the language team consults with formalization experts (which are part of the Rust project themselves) all the time (and formalization or semi-formalization projects are ongoing), and also the mathematical understanding of system languages itself has advanced.
If you could be trusted to do that, we wouldn't need rust in the first place....
The basic contradiction of the rust fad, coders can't be trusted to be memory safe so those same coders must use rust and then all of sudden they can be trusted not to make common mistakes. And before some tart steps in to bring up safe rust, you're missing my point entirely
I asked myself, How many comments to do I have to collapse before someone says something about AI. 3.
I used to compare this hype to crypto hype, but its so much worse. Can we just try not to shove llms into every single conversation.
Is there a hackernews type space where the word is banned? Even lobste.rs has this problem. I need some sort or way to just hide all content on certain sites where LLMs/AI are mentioned.
I'm not a huge AI hype man, but I think you'll just have to accept it. It's a new useful tool, of course people are excited to apply it to everything.
Like it or not, programming will become largely LLMs. And the comment you're replying to is actually making a pretty good case for where the use of LLMs is good: generating code to be formally verified.
Something something halting problem. I never said don't use the tool!! I use the tool too! I just dont want to talk/read about it all the time.
Programming will never be dead.
1. Because the situation you describe is fantasy.
2. Even if it is a reality and all software can be verified (it cant), I will still be programming and so will millions of others because its fun, programming and sex are really damn close to things I cant live without. Not everyone got into engineering for the money. I legitimately love this activity, it is my actual passion. I would rather be poor than give it up.
Its like im being told everyday all day, non stop that the thing I love is not worth loving.
I never said I dont use llms, I have very concrete agent workflows. I work in machine learning. I use thousands in tokens. I've used them since day one. Im not arguing they're not useful, I'm arguing that we can discuss technology without making it about AI every single time.
Its non stop everywhere, nobody is actually thinking about problems, they're thinking if AI could do it for them so they dont have to engage at a high level with anything.
I guess that’s something you need to work through that you’re just so sick of reading about the single biggest evolution in technology since the internet :(
Maybe tech isn’t for you if you don’t like trying to stay on top of it.
Anyways, I probably know more about llms than you, I probably use them more than you. I just dont want to turn every conversation into a discussion about them.
I would argue the smartphone is 1000x more impactful than LLMs, along with many other inventions since the internet. I'm not really sure what contribution llms have had that are actually THAT impactful for peoples lives. Its possibly (but unlikely) a net negative, time will tell. Most people using them are not getting smarter, thats concerning. Most are just making more money for their bosses who are itching to replace them with an llm.
This is remarkable but not super unusual. There are more than 100 issues labeled unsound currently. Some are long standing but from what I understand the new trait solver will unblock fixes for some of them (but probably not the one in OP).
Finding unsoundness bugs isn't the most unusual, yes. But this one is unusual in how simple the code that causes it can be (see the versions of the reproducer code in the comments). For other unsoundness bugs, the code would need to contort itself a lot to avoid the compiler checks.
The idea is that safe Rust promises that you can't cause UB without unsafe.
Unfortunately there are cases, where the current rust compiler implementation fails to keep that promise. These cases are all tracked as bugs and it's expected they'll be fixed eventually. AFAIK non of the known cases is unfixable, it just takes time and effort, sometime a lot.
Also note that C++ does not make such promises in the first place, so the equivalent code there isn't a bug, it's just UB.
I think one social issue I’m seeing is that the Rust community bashes other languages for safety but then glosses over or even completely ignores their own safety risks (see supply chain). I would rather see Rust focus on its actual features without bashing others and maybe start moving away from claiming the gold metal on security. Being less toxic is always a good thing for long term health.
It's important to separate the community ethos and the rust core dev team policies, because I'd be surprised if the official stance of the rust team would be condescending to other technologies.
I’d be shocked if people working on and passionate about thing didn’t shit on other thing. That’s natural and even good in moderation. It’s up to a leader to keep it under control.
Yes. In fact, I have met quite a few humans who make a point NOT to go bashing the work of others. (Of course, I have also met quite a few who do spend their time bashing others.)
Can you give an example of this toxic bashing from rust contributors or are you talking about just random HN posters when you say “rust community”?
Moreover, I wouldn’t say they’re completely ignoring supply chain risks, as there have been discussions about this as early as 2021 [1] and there are ongoing efforts to address this [2]
Yeah Ive actually never seen any Rust team members be toxic. Keep in mind there is a micro niche of tech influencers who try to politicize rust because they associate it with liberalism or something like that and paint Rust community as an opposing force to some status quo they think exists or should exist. Those notions have taken on a life of their own.
People who say this just dont know what they're talking about and are repeating youtubers and X takes.
The emotional reactions to this stuff are so weird. Yeah, software has bugs, what a surprise. That doesn't mean that static safety is useless or that we should all just continue YOLOing stuff in C.
Rust is a cult, the definition of an emotional reaction.
Remember when try catch exceptions were invented and people said coders can no longer ignore errors? How many empty try/catch blocks exist on code today?
Rust doesn't really solve any of the UB in C, and just marks it as "unsafe".... We're back to square one
Worked on a variance-related lint once and the scary part is how rarely anyone writes down variance by hand, so bugs there just sit untested for a decade.
Nobody writes variance at hand in Rust because it's impossible (since before 1.0). You sometimes need to enforce stricter variance than the default (can cause unsoundness and is very subtle but actual unsoundness here is rare) or give more permissive variance (harder and also cannot cause unsoundness, just annoyance).
When implementing the type system, however, variance does have to be treated with care. Historically it wasn't much, now it is.
Took me a good couple minutes to wrap my head around. Man, what a nasty bug. I guess this specific use-case is rare. Time to see if any of the big libs are affected...
A nasty and rare bug can and will be exploited once it is found. The only thing necessary is for malicious actors to start adding this case in innocent looking code and there you have.
That's a misunderstanding. This is not a security vulnerability and Rust explicitly does not defend from malicious programs, only from mistakes. This bug however is quite dangerous, because unlike many soundness bugs it seems plausible to hit by mistake.
> Looking at the bug itself, it is also very likely that this unsoundness has not caused memory unsafety by accident. While it looks easy to trigger, to exploit this you need an intentionally malicious Drop implementation.
struct Q<T: 'static>(Option<T>);
impl<T: 'static> Drop for Q<T> {
fn drop(&mut self) {
// Code in here has access to a non-'static &String
// but assumes that it's a &'static String
}
}
fn main() {
let l = String::new();
let mut q = Q(None);
q.0 = Some(&l);
}
I wonder if the certified compiler for safety critical uses (edit: Ferrocene) has the same issue.
Rust is supposed to guarantee statically that a reference cannot outlive its referent. The `T: 'static` bound means that the value that Q holds must have a 'static lifetime (e.g. either be an owned value or a reference to a static value). So this program should not compile since a reference to l is not 'static. This code is unsound because rust will drop the string l before q so when the Q destructor runs the underlying string has already been freed yet we have a valid reference to it.
$ cat main.c
#include <stdlib.h>
#include <string.h>
struct Q {
/*@null@*/ /*@only@*/ char * t;
};
/*@only@*/
struct Q *
Q_new (/*@only@*/ char * t)
{
struct Q * q = malloc (sizeof *q);
q->t = t;
return q;
}
void
Q_set (struct Q * q, /*@only@*/ char * t)
{
free (q->t);
q->t = t;
return;
}
void
Q_free (/*@only@*/ struct Q * q)
{
free (q->t);
free (q);
return;
}
int
main (void)
{
/*@only@*/ char * l;
/*@only@*/ struct Q * q;
l = strdup ("");
q = Q_new (NULL);
Q_set (q, l);
free (l);
/* This is UB */
Q_free (q);
return EXIT_SUCCESS;
}
$ splint main.c
Splint 3.1.2 --- 21 Feb 2021
main.c: (in function Q_new)
main.c:15:3: Arrow access from possibly null pointer q: q->t
A possibly null pointer is dereferenced. Value is either the result of a
function which may return null (in which case, code should check it is not
null), or a global, parameter or structure field declared with the null
qualifier. (Use -nullderef to inhibit warning)
main.c:14:17: Storage q may become null
main.c: (in function main)
main.c:43:6: Unrecognized identifier: strdup
Identifier used in code has not been declared. (Use -unrecog to inhibit
warning)
main.c:44:13: Null storage passed as non-null param: Q_new (NULL)
A possibly null pointer is passed as a parameter corresponding to a formal
parameter with no /*@null@*/ annotation. If NULL may be used for this
parameter, add a /*@null@*/ annotation to the function parameter declaration.
(Use -nullpass to inhibit warning)
main.c:47:8: Dead storage l passed as out parameter to free: l
Memory is used after it has been released (either by passing as an only param
or assigning to an only global). (Use -usereleased to inhibit warning)
main.c:46:12: Storage l released
main.c:12:1: Function exported but not used outside main: Q_new
A declaration is exported, but not used outside this module. Declaration can
use static qualifier. (Use -exportlocal to inhibit warning)
main.c:17:1: Definition of Q_new
main.c:20:1: Function exported but not used outside main: Q_set
main.c:25:1: Definition of Q_set
main.c:28:1: Function exported but not used outside main: Q_free
main.c:33:1: Definition of Q_free
Finished checking --- 7 code warnings
If you wrote a Q_free function and called it after `free(l);` to actually demonstrate the UAF, that would be pretty close to the semantics of the Rust example.
I originally didn't do this, because I didn't feel the need to invoke UB without necessity. Also I wanted to demonstrate, that the error can (and is) caught in C, without actually committing the double-free (so that the program behaviour is still well-defined, but the abstraction is already violated).
My thoughts as well. The problem can be alleviated either by making the ownership change an error or "just" invoking the destructors in the correct order.
A 'static lifetime constraint on T says: types that satisfy T must not contain any borrowed value/content whose lifetime will be shorter than the life of the program.
So the compiler assumes it is guaranteed, that 'l' still exists, so it doesn't consider it in regard of finalizer ordering.
So Q is a "tuple-struct". In rust you can define a struct like
struct Q<T> {
value: Option<T>
}
with a named field or you can define it like
struct<T> Q(Some<T>)
which is the same struct layout but without an explicit name for the value. In that case, the field is implicitly names `0`
So q.0 = Some(foo) is equivalent to q.value = Some(foo).
The Some(..) is just one variant of the Option enum:
enum Option<T> {
None,
Some(T)
}
Option represents a value that may or may not be initialized. For uninitialized values you use the None variant and then you can initialize it to Some(value).
Some(...) is just constructor for an option type as seen in other languages e.g. java's Optional, haskell's Maybe, c++'s std::optional. I assume that it's needed here because the field can't start as a null pointer otherwise. Maybe the vulnerability still works if the field starts with one string value and swaps to a different string value, but having it start holding None made for a simpler demo.
q.0 is the first field of q, which is anonymous. They could have just as well called it x and written q.x.
'static lifetime bounds are kind of confusing in Rust, but here goes: A 'static lifetime constraint on T says: types that satisfy T must not contain any borrowed value/content whose lifetime will be shorter than the life of the program. So suppose you have a string s, and Option<&String> q. If q has the constraint 'static, and you do q = Some(&s) this should be rejected by the compiler since a reference to s gets a shorter lifetime than 'static by default (you could do q = Some(&'static s) if s is say a string literal or a leaked box but not for a normal string). In the examples it looks like you have to use a tuple to trick the borrow checker but the concept is the same: Rust allowed violation of the 'static lifetime bounds. The drop implemenation demonstrates it: drop happens in reverse declaration order, so the string s gets dropped first. Now q has a dangling reference, a pointer to dropped memory essentially, and we get a pretty classic use after free bug.
chatgpt and grok linked to the the soundness issue, claude I am in usage timeout, and gemini shit the bed as usual: "The compiler rejects the program with error[E0597] on the assignment q.0 = Some(&l)"
Why bother? Most systems these days have over commit and so you can never get an out of memory error. The OS will happily give you more and more RAM, and then when you try to use that memory kill a program (may or not be your program). The only out of memory error you can see is if you are trying to allocate more memory than the address space allows. This is so unlikely that nobody considers it worth bother to try to handle.
It is important to try, for a few reasons. Among other things, increasing amounts of Rust written in the Linux kernel itself, and other environments where you need to take more care with memory allocation.
Rust as a language is capable of that. If you don't use the standard library then you can provide that functionality yourself. The standard library is trying to support it, without creating interfaces that are a massive pain to use.
For instance, it's easy for us to support `Vec::try_reserve`, and we do, but that's not trivial for users to use everywhere; it's error-prone, and it's easy to make a mistake and call a method that goes past your reservation. It's painful for us and for users to make `Vec::push` support this (and having a `try_` variant for every function), so we've been working on a better solution. One current possibility is to have a dedicated type for a Vec that has OOM handling, where `push` can return an error, so you know if you use that type you can never accidentally fail to handle OOM.
the biggest design wart of rust (well one of them) is that support for custom allocators wasn't built into the type system from the start, with allocation osmething that returns Result
Rust is good, I generally do not dislike it - but it does have flaws.
I will happily continue to write things in Golang first. I don't enjoy refactors in Rust, and it's rare that I see things that genuinely need its raw performance.
Cloudflare's Oxy is a stellar example of build in Golang till your design is settled and then port over for performance when you need it.
What the hell. This is not the esoteric, crazy, impractical constellation I expected to find with a title like this. The minimal example is so simple and is definitely something you'd easily come across in normal code.
Afaik loop {} has never been UB, however because llvm started as a c++ compiled where it is, this has been causing miscompilations in rust and C for… nearly two decades (llvm issue 965).
Not at all. There are way more valid lifetimes than the lifetime system of Rust can express. There are countless scenarios where you could accidentally use the unsound behaviour while not producing a segmentation fault because the lifetimes happens to be arranged such that no invalid memory access actually happened.
A program isn't invalid just because it violates the ownership and borrowing rules of Rust. There are tons of programs in the world with shared, mutable access, devoid of Mutexes, Arcs and Locks that nonetheless are completely valid.
Simplified, the point is that a lot of badly typed code that this bug lets through might be mostly harmless (or even fully semantically correct, in some instances). So you can't conclude that 'normal' code wouldn't trigger this bug just because no-one's noticed it until now. The bad code could could be happily executing and performing as expected.
I wonder if the reason it works is because you'd easily come across it in normal code, and someone didn't realize that saving the effort of implementing a check for this would result in unsoundness.
That's not how it works. rustc doesn't "check" for specific cases explicitly, the borrow checker (apparently at fault here by reports) has a set of rules that should reject invalid programs. So either one of the fundamental rules was broken (unlikely here from what I've heard), or some optimization caused the rules to not be implemented correctly.
Not really. I've worked with rust for 4 years, systems side, and never had to write a custom drop implementation. That's the gotcha here, not the rigamarole with the static+Send option type (which _would_ be something you'd encounter in prod).
A custom `Drop` appears very quickly with FFI code. Suppose for example you interface with some C library that expects you to call a function to release some resources.
- "Not really". Implying that your experience generalizes
I've written a bunch of rust programs without custom Drop. I believe your first statement. There are large classes of programs that don't need it. There are also many that do. I think your statement says a lot more about what kind of programs you work on than about custom Drop not being common. People are downvoting the implication that custom Drop is not a common pattern.
No we're in a situation where a bug in the type checker was found and will be fixed and a new release will be made.
That it took 11 years for someone to come across this is a fairly intense counterargument to your attempt to paint this as a language with dangerous footguns.
Here's the weakness of compiled programs. Does this compiled code have this vulnerability? You have no idea. At least with a VM or interpreter you can scan for vulnerable versions and replace the runtime or the specific library.
It's possible to scan compiled programs at the assembly or machine code level. Not enough people do, which is fair enough because it's a slog, but it makes all compiler UB transparent to the analysis.
Old C software is generally more trustworthy than new C software. I don't think this rule of thumb transfers across languages very well. And the definition of new vs old has a fairly large effect. If a language has been under constant change it doesn't matter when it was started a large part of the codebase is "new".
It seems the bug here was caught by Asan instead of at compile time, so basically, for this one bug, rust is reduced to C++-like behavior. You’re still better off using rust because of all the bugs the borrow checker does catch.
The practical upshot to me is that you should be running your rust tests under asan.
It looks like 18 of the 30 issues listed in table 4 had already been fixed when that paper was released, and there is activity in most of the rest. One was recently flagged as being fixed by -Znext-solver, and another has the submitter write that it is fixed, but the issue is not closed. And that's before you consider the impact of the individual issues; how many of the remaining issues impact "real" code?
So I don't think it's fair to claim that "no-one cared".
I don't think "no one cared" is a fair characterisation. The paper doesn't support this conclusion, and from experience I'd say that the two difficulties in fixing unsoundness are doing so without breaking existing code (Rust guarantees stability unless the code is unsound, and introducing previously missing checks can cause sound code to stop compiling, which is a problem if it occurs often) and doing so in a reliable way that can be supported long-term. Rust is currently in the progress of stabilizing next-solver and Polonius, both of which fix multiple long-standing bugs and have been worked on for years now due to intrinsic complexity, performance considerations, compatibility issues, etc. It's not that no one cares, it's just that this stuff is hard and takes time.
I think it has no relevance here at all. Actix was unsound because of prolific use of unsafe. That was a poor design decision but a conscious one. TFA is just a bug.
Type systems are hard! Check out https://counterexamples.org/
I gave it a quick scan for Rust examples; there are 11 samples among the following pages:
The first thing I always look for is mutability (combined with some other tricky feature), e.g. "Now it's a Just(3):Maybe<Int>, now it's a Nothing:Maybe<Int>, now it's a Nothing:Maybe<String>."I wonder if TFA's example could be reproduced without mutability.
"Type systems are hard!" As hard as its safety is pushed on us, not even Rust is free from hand waving.
At least Rust has a chance to be largely correct because it has much greater effort per amount of code (in the compiler) invested into it than most any application code.
"Largely correct" my 2010 python 2 code is "largely correct".
You are saying that there are only incorrect and mathematically proven with nothing meaningful in between?
Not the grandparent you were replying to, but from the note added to the original linked issue (emphasis mine):
> Rust's type system is *intended to prevent memory unsafety. Upholding this promise is something we take very seriously*, .... It is a large priority of the Types Team to *fix all type system unsoundnesses* and to work towards there being a solid foundation to minimize the risk of unknown ones.
So, yes, if you have a group who "takes very seriously" the job to "fix all type system unsoundness", I would expect them to utilize some manner of formal proof verification that their type system is mathematically correct up to some defined limit.
Mathematically correct is not enough.
Java's byte code verification algorithm had a proof. This was important for running untrusted java in the browser. If it said the byte code was ok, it was.
Turns out, nobody made a proof for the verifier actually finishing. So it could return true, or false, or run longer than the universe has time. So around Java 6(?), someone wrote some bytecode that basically took forever to validate, DOSing the validator. Sun had to change the file format and add extra information to get the guarantees back.
No. I am saying you don't need rust for largely correct.
PS: The term you are looking for is formally verified not mathematically proven.
I mean, Rust's whole shtick is safety, so that's really the only thing there is to "push" about the language.
I wouldn’t say so… I consistently choose Rust mainly because it’s a sanely designed modern C++ alternative. It’s 20% more effort than writing Python or Typescript, and you get to use the full power of your hardware without compromise.
Safety is a nice side-benefit. The main reason why I like the safety is because it allows you to fearlessly write high-level code without being constantly paranoid about memory as in C++. It’s more about enabling ergonomics without loosing performance, rather than security or correctness.
Most things like "sanely" and "20%" are pretty subjective. To me writing (or really reading well written) Nim (https://nim-lang.org) is less effort than writing Python or Typescript. Nim is mostly Ada & Lisp ideas packaged in a more terse & flexible surface syntax. Nim also has nice compile-time introspection and very low effort macros to allow packaging near zero-code APIs like github.com/c-blake/cligen. Also, something like 5 out of 5 times I've investigated some Rust alternative to some Nim code, the Rust ran more slowly than my Nim on my tested CPUs.
With access to inline asm, all speed is ultimately more a measure of effort applied than PLang. So those perf ideas are just "with my level of effort". Even Python via Cython has pretty direct access to asm. The "do it in pure X" that Sun popularized (even in a meta-/cross-PLang-sense) as a business attempt to define Java virtual machines as The platform has had many casualties, not the least of which is the quality of discussion of PLang practicalities, not just on HN, but everywhere.
The paranoia about memory use in C++ should mostly be a thing of the past if you’re using smart pointers and sane patterns. In 2026 almost nobody should be calling new and delete and passing around raw pointers.
The reality though it many people are not using smart pointers. I have seen many people argue they don't like them because they want to see every place delete is called. (meanwhile of course they never notice all the places it should be called but isn't - but at least where it is they see it)
Personally I love to use smart pointers where bleeding edge performance is not necessary.
If I need the absolute fastest code, then that code will be tortured under valgrind. That’s non-negotiable in my book.
Code is not done until its memory management is proven correct.
And yet applications written in modern C++ are constantly discovering new memory safety issues. Sean Baxter wrote a whole manifesto talking about the shortcomings of the existing C++ model [0].
[0] https://safecpp.org/draft.html
C++ still doesn't have a sane modern pattern for tagged unions. If you want to define a type to represent, say, a simple parse tree, then Rust makes that easy and obvious, whereas C++ offers you a hundred options, all of which suck.
Rust has a lot of things that make it nice to write in. Robust enums and pattern matching are something I miss greatly when I’m back in C++. The trait inheritance system is also very flexible and I miss that. Especially compared to monstrosities like multiple inheritance.
Part of Rust's schtick is also cost free abstractions.
> not even Rust is free from hand waving.
It is moral though, so who cares really.
so what I take from this is that the rust compiler does not guarantee the stuff it claims to. Because new features of the type system is just being yolod instead of formally proven
EDIT: I said new features of the type system and more importantly, their interactions with the ever growing list of other features, not new features in the compiler. Totally different things. The compiler could be perfectly implementing the wrong choice of algorithms in the first place.
There never was formal verification of the entire rust compiler, or even its complete borrow checker/type system. There has been verifications on _subsets_ of them.
Also, a lot of those soundness issues aren't related to new features _at all_, but usually due to poor assumptions made in optimizations.
The soundness bugs _are_ taken seriously though, and are slowly being patched out. A lot of the links in OP are now closed because Rust either changed how it generates code to avoid the issues, or fixed LLVM.
https://github.com/model-checking/verify-rust-std
hm, there's an effort but scoped only to the std
It's terrifically complex: https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty...
not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.
The eventual goal is verification of the full system. Not the implementation, yes, that's infeasible. But this will mean all soundness bugs will be either found and fixed or we'll know how to fix them once they're found. In any way they won't be fundamental (which is believed to be the case today, but not proven).
so why put them in before knowing if they work reliably? That's the YOLO part, to me
The same combination of reasons we've been doing these kinds of heuristic implementations forever:
- people still get value off of an incomplete implementation, because we are allowed to be mindful of the issues (see, eg, UB in C++). In other words, many, many more bugs have been prevented by the borrow checker working as intended than have been caused by it working poorly. It's not particularly close.
- theory almost always moves slower than practice
The mutable state situation pointed out by the grandparent poster was a famous issue in typing SML under mutability that required serious changes in the language, see Section 4.2 here: https://smlfamily.github.io/history/SML-history.pdf
These were Turing-award caliber people figuring it out and, according to your definition, "yolo"ed it. This stuff is _hard_, and these driveby comments truly aren't helpful.
Because there’s real value delivered even before that? Perfect bring the enemy of good and all that
You're claiming that this bug that reproduces back to Rust 1.4 (2015) is a sign they're adding too many features to make sure they don't introduce bugs? Or do you have bugs that are due to these recent features?
It holds that ¬(∀subsets: isverified(subset)) but it's not true that ∀subsets: ¬isverified(subset), which it think most people would interpret "the whole system is unverified" as
If I independently verify that subsystem A properly consumes apples, and that subsystem B is properly emitting oranges, but never verify that subsystem A is receiving apples, and just connect subsystem B to it, then yeah, the system is not verified.
Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.
Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?
No mainstream compiler is formally proven. If you want a verified compiler, you pretty much have to choose between using a subset of standardml or a subset of C and the one proven compiler for each.
You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"
But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.
They probably meant things like LLVM and the various optimization passes. None of those are verified, there’s probably all sorts of correctness issues, and yet it’s still ok. Rust’s usage also has issues and bugs emitting the right intermediate form for LLVM to consume and usually also it’s ok.
Would it be nice if we had even higher level of quality? Yes. But what’s neat is we have empirical evidence - Rust code does achieve the memory safety goals over C++ even though there’s bugs in the compiler. That’s why Rust is very quickly eating all things C and C++. A huge amount of value that the industry would just be unable to access for a long time if you waited for everything to be formally proven.
Wait, there's a proven subset of C? Can you point me to some info?
https://en.wikipedia.org/wiki/CompCert
There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.
That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms
Tests are not perfect, but they are a lot better than where we were in 1990.
completely tangential to whether you're testing for the right thing.
We are a lot closer to testing the right thing today than we were in 1990!
There are pros and cons to tests, but they do some things very well. For starters a test is a lot better sign that things work as intended than a formal proof which is often so abstract most people can't be sure how it relates to what was intended. You can prove something correct that is clearly wrong. While a test will only test the one case, at least it is typically easy to understand that case and why that answer is correct. Of course if your requirements are correct your proof will tell you it is correct for all cases while a test is limited to that one case. Again pros and cons, and people speaking against tests are not honest about those.
The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.
While true, there are two important differences:
1) Unsoundnesses in Java's type system are checked at runtime.
2) They (or at least some) are intentional or at least won't-fix bugs.
Both are not true for Rust.
As you can see, this is a true statement, but HN really really really hates it for some reason.
Yes. When people describe Rust as "a memory-safe programming language" they are describing an aspirational vision, and not a programming language that has actually been designed with sufficient rigor to guarantee memory safety. Any failure of rustc to actually guarantee this is just a bug in rustc itself, a failure to properly implement the Rust spec, because the closest thing Rust has to a spec is literally just the vague ideal that the compiler should guarantee safety somehow.
Rust cannot fail, it can only be failed.
> Rust cannot fail, it can only be failed.
“Please build the perfect system. Because I specified ‘perfect’ any flaws are due to your incomplete implementation, not my awful brief.”
If the person writing the rust spec was a client I would have to drop them because they would be setting themselves up for dissatisfaction.
I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.
Not to talk about Go, which has intentional unchecked-at-runtime UB (data races) yet many argue to consider it memory safe (and I have a feeling that the same people arguing Rust isn't memory safe are also there. Just a feeling though).
Would you say the same thing about Java? It’s type system is also unsound.
but it isn't claiming to be saving you from things it can't prove it can either.
I'm not an expert on the Java specification, but my understanding is that Java as a language is well-defined enough that we can say things like "Java's type system is unsound", independently from any specific implementation of Java.
You can't do that with Rust because "Rust's type system" is literally just the vague concept of "a type system that is safe". The implementation of this ideal in rustc can have flaws, but Rust itself cannot, because Rust itself has no flaws by definition.
It is true that Rust does not have a complete formal specification for its type system which has been analyzed and proven to be sound.
You seem to be implying that because of this, Rust has no definition of its type system (other than whatever happens to be implemented in the current compiler). I would disagree.
As evidence, I would like to point out that not a single person argued that this flaw was not a bug, but was in fact the officially defined behavior. Clearly, the community has a shared understanding of what Rust's type system "ought" to do.
>Rust cannot fail, it can only be failed...
Sweet. But why should anyone care..
It's surprising this bug went unnoticed for so long, but at least it's easy to fix, since it's not a bug with the type system itself; it's just a bug in the compiler. The compiler should always have been rejecting that code according to lifetime rules of Rust's type system, so the fix is to just make it reject the code, rather than having to change the fundamental rules of lifetimes.
It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against. Rust mitigated this problem a lot in practice, but you can never be certain because of issues like this in practice. This is similar that a math proof that's already been peer reviewed and accepted as truth, may still be possible to be wrong, although the chance is very small but it's not zero. Epseicially when the complexity gets higher.
... and even if you formalize it, it could still be false due to an error in the theorem prover itself.
Not knowing anything about rust, the problem in these type of case is making it rejecting that bad code without also rejecting valid programs. But maybe this is indeed easy to fix, I don't know.
There are no such valid programs. Proof by contradiction:
A valid program would be exploiting undefined behavior in rust, but rust has no undefined behavior. Thus such a program must not exist.
Now a program may appear to work before the fix, but it was never a valid Rust program.
I can't tell if you are sarcastic, but in case you are not:
By Rice's theorem you cannot be sound and complete, i.e. accept all valid programs and reject all invalid ones. Most languages choose to be sound but not complete, i.e. reject all invalid programs but also some valid ones (C and C++ are the notable exception, although most languages have escape hatches). GP was saying that the fix might reject valid programs that compile today. This is true for some existing soundness bugs, but not necessarily for this one specifically.
In this case the issue is that the compiler just isn't properly type checking the implicit call to the drop method that's inserted at the end of the nested block. AFAIK, no correct code should depend on the absence of that check.
Perhaps ironically, AI-based searching of the Rust compiler for bugs is likely to find more of these, pushing Rust closer and closer to the point of complete reliability.
The eventual formalization of Rust and a creation of a formally proven compiler is presumably going to be the end point of this process.
Why would that be ironic? AI is helping us find so many subtle bugs and isolate the root cause, it’s nearly perfect for this type of use case.
> complete reliability.
I think that’s a myth! What tends to happen in mature software is there are unfixable tradeoffs that can be made that favor one use case or another. And of course people will keep adding features too
That’s why they said “closer”
What aspects of it are remotely ironic?
Obviously, many people have viewed AI’s contribution to programming as just producing unreliable garbage.
Yes, that’s an incomplete and tenuous belief, but that’s where the irony is. If you’re omniscient you don’t get to experience irony.
Hey, if Alanis Morissette can make the same mistake…
Until they find bugs in the formal proof program ;)
https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical...
The UB goes all the way down!
Or we realize that it is not possible, and Rust accepts to be "just" a definitely safer C.
There is a formally proven compiler for a large subset of C, so I don't see why formalizing (a large subset of) rust and making a formally proven compiler shouldn't be possible
There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.
Also unlike C, it should be possible to formalize all of Rust, not just a subset. For two reasons: Rust evolution (not initially but today) is strongly tied with formalizing it and the language team consults with formalization experts (which are part of the Rust project themselves) all the time (and formalization or semi-formalization projects are ongoing), and also the mathematical understanding of system languages itself has advanced.
This reminds me of Hilbert’s Program .
Because people want a performant optimizing compiler.
and what stops AI from "accidentally" writing code with such bugs?
Code review and testing? As always?
If you could be trusted to do that, we wouldn't need rust in the first place....
The basic contradiction of the rust fad, coders can't be trusted to be memory safe so those same coders must use rust and then all of sudden they can be trusted not to make common mistakes. And before some tart steps in to bring up safe rust, you're missing my point entirely
I asked myself, How many comments to do I have to collapse before someone says something about AI. 3.
I used to compare this hype to crypto hype, but its so much worse. Can we just try not to shove llms into every single conversation.
Is there a hackernews type space where the word is banned? Even lobste.rs has this problem. I need some sort or way to just hide all content on certain sites where LLMs/AI are mentioned.
I'm not a huge AI hype man, but I think you'll just have to accept it. It's a new useful tool, of course people are excited to apply it to everything.
Like it or not, programming will become largely LLMs. And the comment you're replying to is actually making a pretty good case for where the use of LLMs is good: generating code to be formally verified.
Thank you for citing the Anthropic propaganda manual!
Something something halting problem. I never said don't use the tool!! I use the tool too! I just dont want to talk/read about it all the time.
Programming will never be dead.
1. Because the situation you describe is fantasy.
2. Even if it is a reality and all software can be verified (it cant), I will still be programming and so will millions of others because its fun, programming and sex are really damn close to things I cant live without. Not everyone got into engineering for the money. I legitimately love this activity, it is my actual passion. I would rather be poor than give it up.
Its like im being told everyday all day, non stop that the thing I love is not worth loving.
This seems more like you projecting what you want in terms of what you enjoy and hoping the world optimises around that preference.
The truth is LLMs is what you need to be optimising around as they will become the standard.
I never said I dont use llms, I have very concrete agent workflows. I work in machine learning. I use thousands in tokens. I've used them since day one. Im not arguing they're not useful, I'm arguing that we can discuss technology without making it about AI every single time.
Its non stop everywhere, nobody is actually thinking about problems, they're thinking if AI could do it for them so they dont have to engage at a high level with anything.
Why don't you start TruthLLM like Trump started TruthSocial?
You need to bow in the direction of Silicon Valley every three hours or the inquisition comes.
I guess that’s something you need to work through that you’re just so sick of reading about the single biggest evolution in technology since the internet :(
Maybe tech isn’t for you if you don’t like trying to stay on top of it.
Huh...
Anyways, I probably know more about llms than you, I probably use them more than you. I just dont want to turn every conversation into a discussion about them.
I would argue the smartphone is 1000x more impactful than LLMs, along with many other inventions since the internet. I'm not really sure what contribution llms have had that are actually THAT impactful for peoples lives. Its possibly (but unlikely) a net negative, time will tell. Most people using them are not getting smarter, thats concerning. Most are just making more money for their bosses who are itching to replace them with an llm.
This is remarkable but not super unusual. There are more than 100 issues labeled unsound currently. Some are long standing but from what I understand the new trait solver will unblock fixes for some of them (but probably not the one in OP).
Finding unsoundness bugs isn't the most unusual, yes. But this one is unusual in how simple the code that causes it can be (see the versions of the reproducer code in the comments). For other unsoundness bugs, the code would need to contort itself a lot to avoid the compiler checks.
Wait, shock! So you say rust is unsafe by default?
Not really.
The idea is that safe Rust promises that you can't cause UB without unsafe.
Unfortunately there are cases, where the current rust compiler implementation fails to keep that promise. These cases are all tracked as bugs and it's expected they'll be fixed eventually. AFAIK non of the known cases is unfixable, it just takes time and effort, sometime a lot.
Also note that C++ does not make such promises in the first place, so the equivalent code there isn't a bug, it's just UB.
I think one social issue I’m seeing is that the Rust community bashes other languages for safety but then glosses over or even completely ignores their own safety risks (see supply chain). I would rather see Rust focus on its actual features without bashing others and maybe start moving away from claiming the gold metal on security. Being less toxic is always a good thing for long term health.
It's important to separate the community ethos and the rust core dev team policies, because I'd be surprised if the official stance of the rust team would be condescending to other technologies.
Have you met humans?
I’d be shocked if people working on and passionate about thing didn’t shit on other thing. That’s natural and even good in moderation. It’s up to a leader to keep it under control.
Yes. In fact, I have met quite a few humans who make a point NOT to go bashing the work of others. (Of course, I have also met quite a few who do spend their time bashing others.)
> being less toxic
There's a difference between people you disagree with and toxic behavior. Can you give examples of toxic behavior?
Can you give an example of this toxic bashing from rust contributors or are you talking about just random HN posters when you say “rust community”?
Moreover, I wouldn’t say they’re completely ignoring supply chain risks, as there have been discussions about this as early as 2021 [1] and there are ongoing efforts to address this [2]
[1] https://internals.rust-lang.org/t/about-supply-chain-attacks...
[2] https://kerkour.com/fixing-rust-supply-chain-security
Yeah Ive actually never seen any Rust team members be toxic. Keep in mind there is a micro niche of tech influencers who try to politicize rust because they associate it with liberalism or something like that and paint Rust community as an opposing force to some status quo they think exists or should exist. Those notions have taken on a life of their own.
People who say this just dont know what they're talking about and are repeating youtubers and X takes.
There's a fanaticism amongst Rust devs that borders on a cult. They even described their thinking as such, unironically.
Even the basic logic is flawed.... That coders can't be trusted to handle pointers, but somehow can be trusted to write "safe" unsafe rust.
Dream on
I feel like these things get waved around as gotchas without any sense for whether any real code is impacted.
It will be interesting to see if fixing this bug actually causes any crates to not compile.
We should know shortly, the PR to fix this will presumably be paired a crater run, a build of the entire public crates universe.
The question is. If rust used rust would that have prevented this?
Rust does not prevent all bugs, only certain ones (that are common and dangerous).
no
The emotional reactions to this stuff are so weird. Yeah, software has bugs, what a surprise. That doesn't mean that static safety is useless or that we should all just continue YOLOing stuff in C.
Rust is a cult, the definition of an emotional reaction.
Remember when try catch exceptions were invented and people said coders can no longer ignore errors? How many empty try/catch blocks exist on code today?
Rust doesn't really solve any of the UB in C, and just marks it as "unsafe".... We're back to square one
I'm sure we'll get more of those on other languages / frameworks too. I tend to believe that it's for good
Worked on a variance-related lint once and the scary part is how rarely anyone writes down variance by hand, so bugs there just sit untested for a decade.
Nobody writes variance at hand in Rust because it's impossible (since before 1.0). You sometimes need to enforce stricter variance than the default (can cause unsoundness and is very subtle but actual unsoundness here is rare) or give more permissive variance (harder and also cannot cause unsoundness, just annoyance).
When implementing the type system, however, variance does have to be treated with care. Historically it wasn't much, now it is.
Took me a good couple minutes to wrap my head around. Man, what a nasty bug. I guess this specific use-case is rare. Time to see if any of the big libs are affected...
A nasty and rare bug can and will be exploited once it is found. The only thing necessary is for malicious actors to start adding this case in innocent looking code and there you have.
That's a misunderstanding. This is not a security vulnerability and Rust explicitly does not defend from malicious programs, only from mistakes. This bug however is quite dangerous, because unlike many soundness bugs it seems plausible to hit by mistake.
> it seems plausible to hit by mistake
The report seems to claim the opposite:
> Looking at the bug itself, it is also very likely that this unsoundness has not caused memory unsafety by accident. While it looks easy to trigger, to exploit this you need an intentionally malicious Drop implementation.
This edit is newer than my comment (and its writer is an experienced T-types member, so I take back my words).
The heart of the matter:
I wonder if the certified compiler for safety critical uses (edit: Ferrocene) has the same issue.Can someone ELI5 for people who don't know Rust (but e.g. C)?
Rust is supposed to guarantee statically that a reference cannot outlive its referent. The `T: 'static` bound means that the value that Q holds must have a 'static lifetime (e.g. either be an owned value or a reference to a static value). So this program should not compile since a reference to l is not 'static. This code is unsound because rust will drop the string l before q so when the Q destructor runs the underlying string has already been freed yet we have a valid reference to it.
So the equivalent in C would be:
(The equivalent warning is main.c:47)If you wrote a Q_free function and called it after `free(l);` to actually demonstrate the UAF, that would be pretty close to the semantics of the Rust example.
I have added that now.
I originally didn't do this, because I didn't feel the need to invoke UB without necessity. Also I wanted to demonstrate, that the error can (and is) caught in C, without actually committing the double-free (so that the program behaviour is still well-defined, but the abstraction is already violated).
> rust will drop the string l before q
Why?
My thoughts as well. The problem can be alleviated either by making the ownership change an error or "just" invoking the destructors in the correct order.
But I think https://news.ycombinator.com/item?id=50072252 answers it:
So the compiler assumes it is guaranteed, that 'l' still exists, so it doesn't consider it in regard of finalizer ordering.What does "q.0" and "Some(...)" mean?
So Q is a "tuple-struct". In rust you can define a struct like
struct Q<T> { value: Option<T> }
with a named field or you can define it like
struct<T> Q(Some<T>)
which is the same struct layout but without an explicit name for the value. In that case, the field is implicitly names `0`
So q.0 = Some(foo) is equivalent to q.value = Some(foo).
The Some(..) is just one variant of the Option enum:
enum Option<T> { None, Some(T) }
Option represents a value that may or may not be initialized. For uninitialized values you use the None variant and then you can initialize it to Some(value).
The C rough equivalent would be
struct Q { void* value; }
struct Q q = q { NULL }; q->value = ...
Some(...) is just constructor for an option type as seen in other languages e.g. java's Optional, haskell's Maybe, c++'s std::optional. I assume that it's needed here because the field can't start as a null pointer otherwise. Maybe the vulnerability still works if the field starts with one string value and swaps to a different string value, but having it start holding None made for a simpler demo.
q.0 is the first field of q, which is anonymous. They could have just as well called it x and written q.x.
"Some(...)" means that this Option<T> does have a value of type T in it; "None" means it doesn't.
"q.0" is not really needed, it's a struct with unnamed fields. Here is the same with named fields:
'static lifetime bounds are kind of confusing in Rust, but here goes: A 'static lifetime constraint on T says: types that satisfy T must not contain any borrowed value/content whose lifetime will be shorter than the life of the program. So suppose you have a string s, and Option<&String> q. If q has the constraint 'static, and you do q = Some(&s) this should be rejected by the compiler since a reference to s gets a shorter lifetime than 'static by default (you could do q = Some(&'static s) if s is say a string literal or a leaked box but not for a normal string). In the examples it looks like you have to use a tuple to trick the borrow checker but the concept is the same: Rust allowed violation of the 'static lifetime bounds. The drop implemenation demonstrates it: drop happens in reverse declaration order, so the string s gets dropped first. Now q has a dangling reference, a pointer to dropped memory essentially, and we get a pretty classic use after free bug.
> I wonder if the certified compiler for safety critical uses has the same issue.
It uses the same code, so yes.
(Although I don't know what are their guidelines, it might be that they require avoiding code relying on implied bounds, for example).
which compiler?
Ferrocene
DeepSeek v4.1 Flash thinks it should NOT compile. Whereas in reality it DOES compile which is why it is filed as a bug.
They're seriously using AI as a judge for what to file?
The issue and none of the comments mention AI. It is pretty clear your parent said it by themselves.
I was just checking what outcome an LLM would have based on the patterns in its probabilistic distribution it has seen the wild.
Most LLMs would probably say this piece of code won't compile.
chatgpt and grok linked to the the soundness issue, claude I am in usage timeout, and gemini shit the bed as usual: "The compiler rejects the program with error[E0597] on the assignment q.0 = Some(&l)"
I just wish Rust handled out of memory more gracefully like a normal error.
Why bother? Most systems these days have over commit and so you can never get an out of memory error. The OS will happily give you more and more RAM, and then when you try to use that memory kill a program (may or not be your program). The only out of memory error you can see is if you are trying to allocate more memory than the address space allows. This is so unlikely that nobody considers it worth bother to try to handle.
It is important to try, for a few reasons. Among other things, increasing amounts of Rust written in the Linux kernel itself, and other environments where you need to take more care with memory allocation.
Rust as a language is capable of that. If you don't use the standard library then you can provide that functionality yourself. The standard library is trying to support it, without creating interfaces that are a massive pain to use.
For instance, it's easy for us to support `Vec::try_reserve`, and we do, but that's not trivial for users to use everywhere; it's error-prone, and it's easy to make a mistake and call a method that goes past your reservation. It's painful for us and for users to make `Vec::push` support this (and having a `try_` variant for every function), so we've been working on a better solution. One current possibility is to have a dedicated type for a Vec that has OOM handling, where `push` can return an error, so you know if you use that type you can never accidentally fail to handle OOM.
the biggest design wart of rust (well one of them) is that support for custom allocators wasn't built into the type system from the start, with allocation osmething that returns Result
There is a collection of these someplace. Rust is better but it'll never be perfect, news at 10
Rust is good, I generally do not dislike it - but it does have flaws.
I will happily continue to write things in Golang first. I don't enjoy refactors in Rust, and it's rare that I see things that genuinely need its raw performance.
Cloudflare's Oxy is a stellar example of build in Golang till your design is settled and then port over for performance when you need it.
And a fork fixed it before upstream rust :)
What the hell. This is not the esoteric, crazy, impractical constellation I expected to find with a title like this. The minimal example is so simple and is definitely something you'd easily come across in normal code.
For a long time `loop {}` was undefined behavior. Lots of l-unsounds are really nuts but a few are not.
The reality is that if this were actually code that people wrote, well, it wouldn't have sat around for a decade.
Afaik loop {} has never been UB, however because llvm started as a c++ compiled where it is, this has been causing miscompilations in rust and C for… nearly two decades (llvm issue 965).
Since the Rust language is defined by the Rust compiler and has no other specification, if it's UB in the compiler then it's UB in the language.
And this, kids, is how you get called Billy Madison.
May god have mercy on your soul, cowlevel1.
Rust has no formal spec? Really?
> is definitely something you'd easily come across in normal code.
The fact that nobody reported this before means it's not, by definition.
Not at all. There are way more valid lifetimes than the lifetime system of Rust can express. There are countless scenarios where you could accidentally use the unsound behaviour while not producing a segmentation fault because the lifetimes happens to be arranged such that no invalid memory access actually happened.
A program isn't invalid just because it violates the ownership and borrowing rules of Rust. There are tons of programs in the world with shared, mutable access, devoid of Mutexes, Arcs and Locks that nonetheless are completely valid.
I think you are talking about a different problem and that has nothing to do with my comment.
Simplified, the point is that a lot of badly typed code that this bug lets through might be mostly harmless (or even fully semantically correct, in some instances). So you can't conclude that 'normal' code wouldn't trigger this bug just because no-one's noticed it until now. The bad code could could be happily executing and performing as expected.
I wonder if the reason it works is because you'd easily come across it in normal code, and someone didn't realize that saving the effort of implementing a check for this would result in unsoundness.
That's not how it works. rustc doesn't "check" for specific cases explicitly, the borrow checker (apparently at fault here by reports) has a set of rules that should reject invalid programs. So either one of the fundamental rules was broken (unlikely here from what I've heard), or some optimization caused the rules to not be implemented correctly.
Not really. I've worked with rust for 4 years, systems side, and never had to write a custom drop implementation. That's the gotcha here, not the rigamarole with the static+Send option type (which _would_ be something you'd encounter in prod).
I've written dozens of custom Drop implementations. Well, many of them are named cleanup because of the async Drop mess in Rust, but...
How many of them only conditionally implement Drop, based on a generic param lifetime?
Why would you ever conditionally custom impl Drop? I don't think I've ever seen that pattern, and I can't think of a use case.
OK. That's good to know. I'm not sure why sharing our professional experience with this type of code is controversial, but here we are.
That's easily the exception rather than the rule. I've seen custom `Drop` implementations in almost every non-trivial Rust codebase I worked on.
A custom `Drop` appears very quickly with FFI code. Suppose for example you interface with some C library that expects you to call a function to release some resources.
Now we are at the phase where, Rust is “safe” but only if you use it “correctly” and without using X language feature or a custom Y feature.
This is the problem when a language advertises with “guarantees” and it turns out it never had any due to many false assumptions by their promoters.
So what other soundness bugs are there in the language that we need to know about?
I'm not defending rust here - a correctness bug invalidates the premise. But I am saying that I've never seen a custom drop in production.
For some reason this is controversial, but it remains true.
You said/implied 2 things:
- you've never written a custom Drop
- "Not really". Implying that your experience generalizes
I've written a bunch of rust programs without custom Drop. I believe your first statement. There are large classes of programs that don't need it. There are also many that do. I think your statement says a lot more about what kind of programs you work on than about custom Drop not being common. People are downvoting the implication that custom Drop is not a common pattern.
Custom drops are all over the place. As others have said.
But not custom drops that are doing variadic type stuff like this, usually.
No we're in a situation where a bug in the type checker was found and will be fixed and a new release will be made.
That it took 11 years for someone to come across this is a fairly intense counterargument to your attempt to paint this as a language with dangerous footguns.
Here's the weakness of compiled programs. Does this compiled code have this vulnerability? You have no idea. At least with a VM or interpreter you can scan for vulnerable versions and replace the runtime or the specific library.
With this you have to recompile everything
It's possible to scan compiled programs at the assembly or machine code level. Not enough people do, which is fair enough because it's a slog, but it makes all compiler UB transparent to the analysis.
That is less and less true by the day, for better or worse.
I don't understand how something like this could take so long to be discovered. Pretty crazy stuff.
> I don't understand how something like this could take so long to be discovered.
Maybe they wrote it in C :-)
On a serious note, old software is generally more trustworthy than new software, because bugs are discovered over time and with usage.
Old C software is generally more trustworthy than new C software. I don't think this rule of thumb transfers across languages very well. And the definition of new vs old has a fairly large effect. If a language has been under constant change it doesn't matter when it was started a large part of the codebase is "new".
Because it's rarely used like this, just like weird bugs caused by edge cases found in all kinds of software in the world.
so now what? back to c++?
It seems the bug here was caught by Asan instead of at compile time, so basically, for this one bug, rust is reduced to C++-like behavior. You’re still better off using rust because of all the bugs the borrow checker does catch.
The practical upshot to me is that you should be running your rust tests under asan.
very very good job
This should not be a surprise at all given the amount of soundness bugs that were collected in the Rust compiler but no-one cared. [0]
EDIT: I don’t even think HN cared either up until now. If you search this paper on HN, guess who posted it?
Lets hope that this will be the only occurrence of soundness bugs in Rust and perhaps it needs a tiny disclaimer on claims of “safety guarantees”.
[0] https://arxiv.org/abs/2608.28713
It looks like 18 of the 30 issues listed in table 4 had already been fixed when that paper was released, and there is activity in most of the rest. One was recently flagged as being fixed by -Znext-solver, and another has the submitter write that it is fixed, but the issue is not closed. And that's before you consider the impact of the individual issues; how many of the remaining issues impact "real" code?
So I don't think it's fair to claim that "no-one cared".
I don't think "no one cared" is a fair characterisation. The paper doesn't support this conclusion, and from experience I'd say that the two difficulties in fixing unsoundness are doing so without breaking existing code (Rust guarantees stability unless the code is unsound, and introducing previously missing checks can cause sound code to stop compiling, which is a problem if it occurs often) and doing so in a reliable way that can be supported long-term. Rust is currently in the progress of stabilizing next-solver and Polonius, both of which fix multiple long-standing bugs and have been worked on for years now due to intrinsic complexity, performance considerations, compatibility issues, etc. It's not that no one cares, it's just that this stuff is hard and takes time.
Poor Rustees no longer see the bugs due to the syntax noise!
wonder what happened to this https://raphlinus.github.io/rust/2020/01/18/soundness-pledge...
I think it has no relevance here at all. Actix was unsound because of prolific use of unsafe. That was a poor design decision but a conscious one. TFA is just a bug.
Having ideals does not mean there are never bugs.
What do you mean?