Remix.run Logo
Remix clone Hacker News
new | show | ask | jobsGithub
▲ mrkeen 4 hours ago

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 3 hours ago | parent | next [-]

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.

▲roblabla 3 hours ago | parent | next [-]

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.

▲meltyness 2 hours ago | parent | next [-]

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

▲vrighter 2 hours ago | parent | prev [-]

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.

▲afdbcreid an hour ago | parent | next [-]

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

▲vrighter an hour ago | parent [-]

so why put them in before knowing if they work reliably? That's the YOLO part, to me

▲cscheid 7 minutes ago | parent | next [-]

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.

▲dwattttt 7 minutes ago | parent | prev | next [-]

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?

▲vlovich123 4 minutes ago | parent | prev [-]

Because there’s real value delivered even before that? Perfect bring the enemy of good and all that

▲streetfighter64 2 hours ago | parent | prev [-]

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

▲vrighter an hour ago | parent [-]

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.

▲thfuran 3 hours ago | parent | prev | next [-]

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.

▲vrighter 2 hours ago | parent | next [-]

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.

▲AnimalMuppet 2 hours ago | parent | prev [-]

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

▲xgk 2 hours ago | parent | next [-]

https://en.wikipedia.org/wiki/CompCert

▲ 2 hours ago | parent | prev | next [-]
[deleted]
▲ 2 hours ago | parent | prev [-]
[deleted]
▲jeremyjh 3 hours ago | parent | prev | next [-]

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

▲vrighter 2 hours ago | parent | next [-]

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

▲bluGill 2 hours ago | parent [-]

Tests are not perfect, but they are a lot better than where we were in 1990.

▲vrighter an hour ago | parent [-]

completely tangential to whether you're testing for the right thing.

▲carlmr 2 hours ago | parent | prev [-]

[flagged]

▲_flux 2 hours ago | parent | next [-]

I think the difference is here:

- If a compiled C++ program has unsound behavior, the program needs to be fixed

- If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

▲bonzini 24 minutes ago | parent | next [-]

> - If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

Not really: the program still needs to be fixed, but fixing the compiler ensures that this unsound behavior never happens again for everyone.

▲jooops1 an hour ago | parent | prev | next [-]

That's not completely correct. If the Rust or C++ compiler has a bug in both cases either the compiler has to be fixed or the program can be adjusted to work around said compiler bug If possible. However, It's fair to argue that the Rust compiler makes more assertions and is more complex, which results in a larger error surface.

▲afavour an hour ago | parent | prev | next [-]

Which is better, surely? One fix for every program written in Rust vs everyone having to fix it themselves…

▲devmor 2 hours ago | parent | prev [-]

> If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

Can you provide an example of such a program that can’t be fixed at the program level like a C++ example?

▲_flux 2 hours ago | parent [-]

Sure, usually the program can be changed to avoid the issue, but the key here is that the Rust compiler is wrong and needs to be fixed. Once fixed, the actual program fix also falls in place, as it cannot be compiled anymore.

▲krona 2 hours ago | parent | prev [-]

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

For what it's worth, Rust fanboys also seem just as vulnerable to their ignorance of C/C++ compiler extensions and tooling (e.g. sanitizers, bounds annotations, standard library hardening modes and so on.) which are just normal part of professional C/C++ use today.

▲afdbcreid an hour ago | parent [-]

And are also woefully insufficient as proven in most sanitized & linted & fuzz-tested programs in existence (browsers and operating systems).

▲krona an hour ago | parent [-]

Compared to what? CVE-2025-68260?

▲afdbcreid an hour ago | parent [-]

Compared to, for example, 5 million Rust lines in Android, I'd say.

▲UncleMeat 2 hours ago | parent | prev | next [-]

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

▲afdbcreid 2 hours ago | parent [-]

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.

▲cowlevel 2 hours ago | parent | prev | next [-]

As you can see, this is a true statement, but HN really really really hates it for some reason.

▲csande17 3 hours ago | parent | prev [-]

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.

▲DriverDaily 2 hours ago | parent | next [-]

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

▲insanitybit 2 hours ago | parent | prev | next [-]

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.

▲afdbcreid 2 hours ago | parent [-]

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

▲ 2 hours ago | parent [-]
[deleted]
▲UncleMeat 2 hours ago | parent | prev | next [-]

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

▲csande17 2 hours ago | parent | next [-]

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.

▲mcherm 36 minutes ago | parent [-]

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.

▲vrighter 2 hours ago | parent | prev [-]

but it isn't claiming to be saving you from things it can't prove it can either.

▲lolakutty 2 hours ago | parent | prev [-]

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

Sweet. But why should anyone care..

▲codehero an hour ago | parent | prev [-]

"Type systems are hard!" As hard as its safety is pushed on us, not even Rust is free from hand waving.

▲ahartmetz an hour ago | parent | next [-]

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.

▲throwawayffffas 36 minutes ago | parent [-]

"Largely correct" my 2010 python 2 code is "largely correct".

▲ahartmetz 18 minutes ago | parent [-]

You are saying that there are only incorrect and mathematically proven with nothing meaningful in between?

▲doodpants an hour ago | parent | prev | next [-]

I mean, Rust's whole shtick is safety, so that's really the only thing there is to "push" about the language.

▲oersted 41 minutes ago | parent | next [-]

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.

▲ryandrake 26 minutes ago | parent [-]

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

▲eloisius 24 minutes ago | parent | prev | next [-]

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.

▲hackingonempty 21 minutes ago | parent | prev [-]

Part of Rust's schtick is also cost free abstractions.

▲caaqil an hour ago | parent | prev [-]

> not even Rust is free from hand waving.

It is moral though, so who cares really.