219 points formerly_proven 2 hours ago 93 comments

vincent-uden 1 hour ago | parent

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.

LoganDark 1 hour ago | parent

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.

jvanderbot 1 hour ago | parent

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

bryanlarsen 1 hour ago | parent

I've written dozens of custom Drop implementations. Well, many of them are named cleanup because of the async Drop mess in Rust, but...

dwattttt 13 minutes ago | parent

How many of them only conditionally implement Drop, based on a generic param lifetime?

jvanderbot 9 minutes ago | parent

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.

neysofu 1 hour ago | parent

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.

gspr 57 minutes ago | parent

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.

rvz 13 minutes ago | parent

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?

jvanderbot 10 minutes ago | parent

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.

cmrdporcupine 7 minutes ago | parent

Custom drops are all over the place. As others have said.

But not custom drops that are doing variadic type stuff like this, usually.

cmrdporcupine 7 minutes ago | parent

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.

insanitybit 1 hour ago | parent

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.

fg137 19 minutes ago | parent

> is definitely something you'd easily come across in normal code.

The fact that nobody reported this before means it's not, by definition.

cowlevel 1 hour ago | parent

Rust is not a memory-safe language. cve-rs proved it years ago but commenters always argue that cve-rs is too contrived to matter, or that it's a compiler bug so it doesn't count.

insanitybit 1 hour ago | parent

lol do you think that cve-rs was required? there is literally an l-unsound tag on rustc's github, this isn't some embarrassing or secret thing.

Safe rust is safe, granting `unsafe` and compiler errors. This isn't a secret.

psychoslave 1 hour ago | parent

What's l- here? Literal?

pas 1 hour ago | parent

insanitybit 28 minutes ago | parent

lol I was writing `l` because I thought it was `labeled-unsound` for like a fucking decade

high_na_euv 1 hour ago | parent

in compare to c and cpp? it is

cowlevel 1 hour ago | parent

And in absolute terms?

qweqwe14 1 hour ago | parent

Literally nothing can be anything in absolute terms, what's your point? The fact is that Rust is miles better than any other language in terms of memory safety & performance ratio. That's all that matters.

high_na_euv 51 minutes ago | parent

cmon, it is time move on.

it has been discussed bilion times

david-gpu 1 hour ago | parent

Let us not conflate a bug in an implementation (rustc) with a defect in the language (Rust).

cowlevel 1 hour ago | parent

Which clause of the language specification is being violated?

lkey 52 minutes ago | parent

Lifetimes can be effectively erased via covariant assignment. It's in the title. Even a beginner could understand these assignments are not in spec? Are you just being contrary to be contrary?

cowlevel 47 minutes ago | parent

So point to the spec

beanjuiceII 39 minutes ago | parent

this is probably a great opportunity for rust to get one, if they want to be taken seriously

uniqueusername7 21 minutes ago | parent

I totally understand that people have favourite languages and that rust, like any language and any ecosystem around that language, has idiosyncrasies that are not for everyone, but how would one ever come to the genuine conclusion that rust is not being taken seriously? By whom?

Ukv 25 minutes ago | parent

https://public-docs.ferrocene.dev/main/specification/types-a...

Specifically the `q.0 = Some(&l);` violating 4.15.2:40 ("An assignment expression requires that the type of its value operand is a subtype of the type of its assignee operand.")

csande17 42 minutes ago | parent

If that's the definition you're using, then C is also a safe programming language. In fact, C is even safer, because it actually does have a specification that lists all the invariants that the programmer has to uphold themselves because the compiler doesn't check them.

mrkeen 1 hour ago | parent

AFAIK there isn't a language spec. Rustc is the language for now.

afdbcreid 58 minutes ago | parent

But bugfixes are also allowed. So the fair conclusion is that the implementation is broken, but the language is not - because it's possible to fix, and it's possible for all known soundness issues (including the cve-rs one). For this one specifically, I've heard people are already working on a fix.

cowlevel 47 minutes ago | parent

If the compiler is the language that implies there is currently a bug in the language, which will be fixed when the compiler is fixed.

david-gpu 54 minutes ago | parent

My understanding is that it is work in progress, via Ferrocene.

beanjuiceII 40 minutes ago | parent

Ferrocene has his same flaw

david-gpu 27 minutes ago | parent

If that's the case then I was wrong.

Hugsbox 1 hour ago | parent

I don't understand how something like this could take so long to be discovered. Pretty crazy stuff.

lelanthran 1 hour ago | parent

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

zaphar 50 minutes ago | parent

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

fg137 18 minutes ago | parent

Because it's rarely used like this, just like weird bugs caused by edge cases found in all kinds of software in the world.

FuzzywarmWalnut 1 hour ago | parent

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.

MrBuddyCasino 1 hour ago | parent

The heart of the matter:

  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.

high_na_euv 1 hour ago | parent

which compiler?

sshine 1 hour ago | parent

Ferrocene

wg0 1 hour ago | parent

DeepSeek v4.1 Flash thinks it should NOT compile. Whereas in reality it DOES compile which is why it is filed as a bug.

jug 1 hour ago | parent

They're seriously using AI as a judge for what to file?

afdbcreid 1 hour ago | parent

The issue and none of the comments mention AI. It is pretty clear your parent said it by themselves.

wg0 1 hour ago | parent

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.

ChickeNES 31 minutes ago | parent

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

afdbcreid 1 hour ago | parent

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

1718627440 26 minutes ago | parent

Can someone ELI5 for people who don't know Rust (but e.g. C)?

thinkharderdev 5 minutes ago | parent

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.

badatnames 1 hour ago | parent

There is a collection of these someplace. Rust is better but it'll never be perfect, news at 10

zer00eyz 1 hour ago | parent

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.

akoboldfrying 1 hour ago | parent

As an old C++ guy, my take is: Heh heh heh.

ETA: Downvoters, I salute you. Without your selfless courage, the forces of light humour would surely prevail.

rvz 1 hour ago | parent

Yeah. A reminder that no language is a silver bullet even if it is heavily marketed. Especially with the “written in XYZ™” tag line.

mrlonglong 1 hour ago | parent

You got my upvote.

wg0 53 minutes ago | parent

You got my upvote and this one decade old issue:

https://github.com/rust-lang/rust/issues/25860

fg137 31 minutes ago | parent

This is not the first soundness bug. Some bugs aren't fixed for years. The Rust community is well aware that such bugs exist, will be found, and address them just like other high impact bugs. In other words, if you paid the slightest attention to the development of Rust language, you would know this is surprising but not unexpected, and has happened many times.

akoboldfrying 13 minutes ago | parent

Given that TFA is currently #1 on HN, I suspect I'm not the only person who is aware of Rust's borrow checker but not aware, until now, that it has a history of serious soundness bugs.

Philpax 21 minutes ago | parent

People in sugar glass houses shouldn't throw stones :P

mrkeen 1 hour ago | parent

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:

  https://counterexamples.org/eventually-nothing.html
  https://counterexamples.org/mutable-matching.html
  https://counterexamples.org/selfishness.html
  https://counterexamples.org/scope-escape.html
  https://counterexamples.org/nearly-universal.html
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.

vrighter 40 minutes ago | parent

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

thfuran 33 minutes ago | parent

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.

AnimalMuppet 5 minutes ago | parent

Wait, there's a proven subset of C? Can you point me to some info?

csande17 28 minutes ago | parent

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.

lolakutty 17 minutes ago | parent

>Rust cannot fail, it can only be failed...

Sweet. But why should anyone care..

UncleMeat 10 minutes ago | parent

Would you say the same thing about Java? It’s type system is also unsound.

insanitybit 5 minutes ago | parent

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.

roblabla 24 minutes ago | parent

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.

jeremyjh 24 minutes ago | parent

There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.

carlmr 5 minutes ago | parent

Spot on, but this makes me think of a larger problem.

You can be annoyed by Rust fanboys, sure, but the more annoying are the Rust haters, because the hate always comes from a place of ignorance.

The hate only works if you don't go beyond a surface level understanding of Rust.

E.g. a niche case on the borrow checker is slightly broken, so borrow checking doesn't make sense.

Or the "oh but Rust needs unsafe, so it's just like C++".

Yeah, but by that measure all of C++ is unsafe++, even unsafe has more guarantees than standard C++.

Only if your whole understanding of the concept is that the keyword is called "unsafe", does that argument make sense.

A bit of a rant, but if you hate Rust with a passion, ask yourself first where that opinion comes from and if it can stand on its own. In most cases it can't.

UncleMeat 11 minutes ago | parent

The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.

rvz 1 hour ago | parent

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?

[0] https://arxiv.org/abs/2608.28713

optionalsquid 1 hour ago | parent

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

purplesyringa 1 hour ago | parent

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.

JABVOLT 1 hour ago | parent

very very good job

j4k0bfr 46 minutes ago | parent

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

beanjuiceII 45 minutes ago | parent

ModernMech 40 minutes ago | parent

What do you mean?

jeremyjh 27 minutes ago | parent

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.

lambdaone 45 minutes ago | parent

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.

bbor 36 minutes ago | parent

Until they find bugs in the formal proof program ;)

https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical...

kimi 23 minutes ago | parent

Or we realize that it is not possible, and Rust accepts to be "just" a definitely safer C.

wongarsu 15 minutes ago | parent

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

UncleMeat 9 minutes ago | parent

Because people want a performant optimizing compiler.

fnord77 39 minutes ago | parent

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

baq 12 minutes ago | parent

That is less and less true by the day, for better or worse.

weinzierl 22 minutes ago | parent

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