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.
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.
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".
> On a serious note, old software is generally more trustworthy than new software, because bugs are discovered over time and with usage.
The age of software means bugs are more likely to be discovered but not necessarily fixed. In the case of Rust, the developers have documented a whole lot of unsoundness bugs that require a new borrow checker architecture to fix.
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.
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 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;
}
int
main (void)
{
/*@only@*/ char * l;
/*@only@*/ struct Q * q;
l = strdup ("");
q = Q_new (NULL);
Q_set (q, l);
free (l);
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:36: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:39: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:38:12: Storage l released
main.c:41:22: Fresh storage q not released before return
A memory leak has been detected. Storage allocated locally is not released
before the last reference to it is lost. (Use -mustfreefresh to inhibit
warning)
main.c:36:2: Fresh storage q created
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
Finished checking --- 6 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).
I'm not familiar with Splint, but my understanding is that the error is because of the @only@ marker indicating that the string is not shared. That's an incorrect translation of the Rust program, where the reference to the string is explicitly a shared reference rather than an owned reference. The issue isn't the sharing; it's that rustc mistakenly allows the code to assign a reference that is valid until the end of the current scope to a field that expects a reference valid forever (like a string constant in the program binary). The Rust program with equivalent semantics to your C program (passing an owned String instead of a shared reference) is correctly rejected by the compiler.
Also, the Q_free function should not free q->t. It may access it (e.g. printing it), but it does not own that reference and is not responsible for deallocating its memory.
Sorry, I should have looked closer the first time! My excuse is that it was too early in the morning to be thinking about such things.
Yes, @only@ means that the parameter/variable is owning. I believed that would have been the meaning in Rust. Now I can no longer edit my comment, oh well.
> Also, the Q_free function should not free q->t.
Well, that's because I thought it would own it. But if in Rust it is not implied that the Q owns the string, then I fail to see where the error is? Both l and q will be deallocated at the end of the main function. Depending on the order of the deallocation maybe q exists for a theoretical time while pointing to already deallocated memory. But both get deallocated at the same point, so q does not outlive the existence of l, so where is the error?
The error is the destructor of `q` could look at the reference and stash it away somewhere, like a global variable (since the compiler thinks the reference is valid forever). Then, some other part of the program could access that variable and cause a UAF.
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.
That's incorrect; the compiler drops q before l. Drops happen in LIFO order; and the compiler knows that it can't drop l before q has been dropped, because q contains a reference to l.
The issue is that the destructor of q can observe a reference which is about to be deallocated as having a 'static lifetime (i.e. it will live forever), and can thus stash it away somewhere for other code to access after it's been freed (as in the examples in the issue which demonstrate UB.)
'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 doubt my read is fully accurate, there's probably a relatively small niche where it occurs. But it does seem to be a rather glaring gap, for how long it has existed.
(All languages have this, this is not a rust bashing. Rust seems to do quite well for how complex it is)
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.
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.
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.
"Serious" soundness bugs? That's a stronger claim, and one that you introduced. So you have the burden of proof. Which of those soundness bugs are serious, and what about them makes them so?
This is not even the first soundness bug that appeared on HN frontpage. It just means you don't pay attention to Rust development, that's it. I don't even use Rust at all yet I know a number of quirks about its compiler.
I hereby confirm that you are 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.
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.
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
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.
Okay, but verifying a type system and language specification for soundness wouldn't actually give you any of the guarantees you want if the compiler toolchain isn't verified to implement them correctly. And this sort of thing just isn't standard practice in the industry and never has been. Sure it would be nice if more things were verified, and we are somewhat headed in that direction, but it seems weird to say that rust specifically is just a bunch of half-baked yoloing because it doesn't do something that essentially no other language is doing 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.
Eh. Java was released in 1995. Smashing the Stack for Fun and Profit was published in 1996. The big selling point for java in the beginning was write-once-run-everywhere. Being a GCed language was also a selling point, but that is distinct from memory safety as a selling point.
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).
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.
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.
you’re deeply confused but the words “validation” and “qualification” may help untangle the web, there’s a lot more to assurance than what your model seems to hold (and you’re drawing batshit deductions from it)
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).
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?
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.
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.
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.
> 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 a vulnerable to their ignorance of C/C++ compiler extensions and tooling (e.g. sanitizers, compiler extensions, standard library hardening modes and so on.) which are just normal part of professional C/C++ use today.
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
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?
Important to note that this is is not a bug in the type system itself, it's a bug in the borrow checker not enforcing invariants that the type system says that it should, and formal verification of the type system would not have helped here.
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.
That work is ongoing even if the RustBelt project ended. It's been a / the major focus of Ralf Jung's work for over 10 years and he's an assistant professor at ETH Zürich now, still working on it. https://www.ralfj.de/blog/categories/research.html
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.
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.
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].
The problem with manefestos is they often harp on small pars that don't matter. There are real shortcoming of the C++ model, but if you use modern C++ they are rare.
The real short coming it is very common for people to not write modern C++. I know several C++ developers who refuse to use smart pointers because they don't like magic happening.
It's not enough for memory safety issues to be "rare". To meet your obligations under the standard and have defined behavior (i.e. rust's basic guarantee), memory safety issues can't exist at all.
Ah, so this article invalidates all of the safety guarantees of rust? Since one hole was found the entire boat is shot and should be left at the bottom of the harbor?
C++ has a terrible reputation which is well associated with, say C++98, if you have a good linter you can bop people on the head for using news anywhere outside a few limited locations where you consider it warranted. All working environments have language features or even programming paradigms that are considered detrimental to code ecosystem health and fighting against these is an organizational lift when working in any programming language. Full type security doesn't mean someone can't create an overly generic object and just start breaking code contracts across the code base. C++ has an awful lot of footguns and more warts than most but it can be made to be sane for development and the new language features really bring it on par with other modern languages.
I have worked in C++ (primarily within the Qt framework which pushed hard into const refs instead of pointers) and it's fine. I've also worked in PHP which can also be fine. Rust isn't something I've worked at scale in but it certainly is very attractive if I ever jump to an org working in it - but even in Rust you'll want to restrict style divergence and bad patterns with linting.
The answer depends on how foo() is implemented. You can't reason about it locally, and strictly speaking it's not possible to determine at compile time. Now, I should be declaring this gsl::not_null<std::unique_ptr<int>> to comply with the core guidelines, but I think we can agree that optional support libraries aren't relevant to this discussion.
That's trivially untrue. Nothing about turing machines or lambda calculus requires temporal unsafety. Even this example wouldn't exist if the compiler rejected covariant lifetimes. You already know this of course, so I'm not going to keep beating that dead horse.
The obvious follow-up is to find a minimal set of rules that allow us to express what we want without permitting temporal unsafety. The borrow checker is one set of fairly minimal rules that works pretty damn well. Alternatively you could define away the unsafety by giving it semantics, like fil-C does.
C++ still doesn't have a sane pattern for tagged unions. If you want to create a type for representing, say, a simple parse tree, then Rust makes that easy and obvious, whereas C++ offers you a hundred options, all of which suck.
I take your point about it being the default, but IMO std::variant is pretty much unusable for a parse tree. It could work for small unions that you visit once in a while, but traversing a nested tree of std::variant types is just hellish.
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)
It's more than that. Smart pointer help, but there are cases where even when using smart pointers you can encounter memory safety issues. Especially when you need to interact with c or older c++ code that doesn't use smart pointers. And smart pointers don't provide any protection against data races in multi-threaded code, like rust does.
I have heard great things about Nim, you may be very right. It’s just that it’s impossible to ignore the benefits of a mainstream dependency ecosystem. The ecosystem is exactly what made Python and Javascript the giants they are today, despite being somewhat mediocre languages. And the Rust ecosystem is in that same league, without giving up exceptional performance, and without giving up too much ergonomics.
PS: I was very enthusiastic about Cython for a good while and I went deep into it, but I found that it is rather a mess to use in practice. Yes you get C performance within Python, kinda, but you also get all the C footguns, amplified by the complex interactions with Python features.
Yeah. Other ecosystems are undeniably larger than Nim's. I keep hearing about how LLMs are going to nullify that advantage with "not so sloppy" ports of anything to any PLang, but I've yet to see that pattern materialize. "What is a clean interface" is probably a kind of subjective judgement call, but also very clearly depends on PLangs and even PLang cultures. For example, the microdependency culture of Rust/JS/Node have very little to do with the PLang's themselves.
This is misinformation. There is (at least!): `method`, procedurally typed fields (inside case-object variants or not), run-time keyed `Table` with proc values, {.dynlib.}, importc/importcpp things. Beyond that, yes, Nim has rare compile-time superpowers that do lead many of its proponents to use static constructs (totally grant that!). So, you may not see a lot of dynamic dispatch in code bases, but there is little stopping you from using them in your own code.
Ah, yes, I should have been more precise. It doesn't have an equivalent of an interface/trait/protocol with dynamic dispatch.
Yes, you can pass around an object of procedures, but that is awkward, doesn't have any support from the language or stdlib, and from what I can tell isn't a normal thing that is done.
I think you & I are really back & forth-ing "the PLang not enforcing/strongly encouraging a very specific way of doing things that a whole ecosystem/community organizes around". Relying instead on self-organization has many pros & cons, to be sure. Lisp suffered much the same "until" Common Lisp (which still leaves many things open). My tag line lately is: delegation affords so much, but trust sure is tricky. Much of the time people seem to discount the often rather large cost of establishing/maintaining trust. (I'm not saying you are - just that it's an easy thing to do.)
> It’s 20% more effort than writing Python or Typescript
I'd disagree with this point, there is more typing involved with a first draft of code than Python or Typescript, that's certainly true, but if we bring all the tools (e.g. docblock comments for "type declaration") that are habitual to make up for the shortcomings in most developer's minds then that gap shrinks and, imo, ends up swapping. It's cheaper to have automatically enforced and consistently maintained checks than moving that information out of band and the resulting code in a strictly typed and memory enforced language ends up removing a significant cognitive overhead when reading and maintaining the code.
I have a strong aversion to boilerplate code so it's important to try and allow terse expressions when possible - but unstated assumptions are worse than overstated assumptions.
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.
Neither C++ nor Rust is zero cost in many cases. Rust needs unsafe or expensive runtime primitives for doubly linked lists, an lru cache, a tree with parent pointers...
Both patch the language gaps with libraries.
Idk, it also has a nicely expressive typesystem outside of lifetimes, a lot of modern syntactic features like pattern matching and monadic error handling, well-written compiler error messages, a well-designed standard library, and substantially less accrued cruft when compared to its largest competitor. Safety might be the cudgel its evangelists like to beat everyone over the head with, but there are certainly things to recommend it outside of that.
https://github.com/JelleZijlstra/unsoundness is also a great collection of Python type system holes. In these cases, it's mostly deliberate design decisions, not bugs. The unfortunate fact is that a fully sound Python type system would be a pain to use.
Perhaps I'm just an old dog that doesn't want to learn new tricks, but I still can't think of Python as typed and I never use type hints. I started with Python during the 2.3 era. I still view Python types as merely docs. So it's nice that someone tracks mypy quirks but I can't imagine relying on the results for anything serious.
To be very pedantic, Python was always strongly typed in the sense that every value has a concrete type. This is very different to, e.g. C, where `void*` is often used to actually erase the type or, conversely, more abstract languages where there are only interfaces.
But of course Python function were always duck typed so it often didn't matter to the user.
If you deal mainly with small-to-medium size Python programs, which is probably the norm, that makes sense to me. But if you have a large Python application, or if you own a library API that might have a lot of callers, typecheckers catch sooo many mistakes.
I've been writing python for closing in on two decades (I want to say maybe 2.5 was my introduction point?).
I've found type hints to be remarkably useful and catch significantly more bugs than I ever would have thought, and have quickly picked up the practice of using them wherever I code. My general finding is that if I have to struggle to put useful type hints in place, I probably need to rethink my code.
I even type hint my unit tests because I've learned that sometimes type incorrectness means my tests haven't been testing what I thought they were testing.
Frameworks like pydantic[0] can help you turn those type hints into something runtime enforcing too.
Generally speaking, static typing is the great enabler of writing bad Python code.
As soon as static typing is introduced into a Python code based, the developers start writing unscalable coding patterns that don't scale to larger programs.
You can't rely on Python's type hints for serious verification, but it can be great for expressing abstractions and giving people (and, today, agents) better affordances for using them. Even static errors that will not always fire can still help a lot for using a library correctly and for noticing mismatches in your codebase as it evolves over time.
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.
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...
And 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.
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.
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.
It is well known that proof assistants can be wrong. Fortunately, the theories underlying formal methods are usually simple enough that it is feasible to write verifiers for these proofs.
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.
You got my reference. But the original comment stands at -1 points now, even mock criticism of C and Rust seems to be totally unappreciated by the bigots.
Yeah this is actually quite interesting. I can see how people who have this "slop generator" perspective on AI would see this as an irony. But to me, it isn't an irony, it's a demonstration of why this perspective on AI is wrong.
I assume that's why the original comment said "perhaps ironically".
I'm firmly in the "AI is incredibly powerful and useful" camp myself, but there's no question that currently, without good human oversight and feedback, AI output can have many issues which can be described as slop.
But yes, improved type systems are one of the ways this can be managed, and essentially help bootstrap more reliable systems.
There's a minor irony in imperfect system being used to help build more perfect systems, but you could say the same thing about human developers.
Yeah I mean I'm not that interested in debating the definition of "irony", but it just doesn't strike me as ironic at all that AI is good at doing the grunt work to expose a bug like this! If you think "wow, it's ironic that AI can be used to improve software quality" instead of "well yeah, this is exactly the kind of thing that AI is good at", then IMO you've got your priors about AI mixed up.
Yeah I can see it too! That's what made it an interesting point to me. I totally recognize there are people out there who see this as an irony. My point is that this is an interesting demonstration of the way in which (IMO) those people are misperceiving things.
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
Even if you could be trusted to do that, we still need languages like Rust and tools like ASAN and Valgrind. Trust but verify. Trust alone is not enough.
The compiler. That’s the whole point here. Type systems can prove the absence of entire classes of bugs, at compile time. If AI identifies bugs in type systems that can be corrected, then all future programs benefit, including those written by AI.
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 see. I'm not trying to put down your love of programming. The only programming that I really can say excites me (C64 or the like) died a long time ago, before I even started I suppose.
Nothing is stopping you from enjoying the sort of programming that you like. But I think it's healthy to accept that that style will soon not be mainstream. It will be like knitting your own clothes, and that's okay.
Regarding formal verification, it's not needed, as LLMs already make on average about as many errors as the average human programmer.
For me, 90% of programming is just a tool to get the job done. It's like a machine in a factory that spits out 50 spoons a minute, and it doesn't need to be any more beautiful than that. If you enjoy woodcarving and want to spend an hour making your own spoon, do that and don't let the existence of the machine make you feel that hobby is any less worth loving.
Unfortunately, a large proportion of stories submitted to Lobste.rs are slopped out... even if they don't mention AI, it's hard to escape there. Hacker News at least has functioning story-level moderation.
Oh that is very nice. I had been thinking about building something like that, happy to see someone beat me to it. Might actually make me check hacker news more frequently again.
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
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.
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.
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.
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.
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 the theorem prover has no errors, the math behind the theorem prover could be inconsistent according to Gödel's incompleteness theorem. So even in principle, we can never be completely certain about the soundness of Rust, though the more theoretical concerns tend to be dwarfed by basic human error.
I think it's a good thing to keep in mind, that the actual implementation of Rust almost certainly isn't sound. Even an "ideal Rust" still has unsafe, which can affect the soundness of even faraway safe code. But I don't think it's nessesarily wrong to talk about Rust as if it were safe. Much of our communication has implicit assumptions, and the way we talk about Rust is no different. It would be exhausting to qualify every discussion of saftey with "assuming the compiler has no bugs", "assuming all unsafe code follows the (not fully specified!) rules", etc.
Ultimately it's like any other implementation of theory into practice. The theoretical model of Rust lets us reason about and design an implementation to achieve certain practical goals even though the model is a simplification of reality. In Rust's case, practical use has demonstrated it achieves design goals like reducing bugs and reducing development time (compared to peers like C++) to a substantial degree.
It’s like Python describing itself as fast. Everyone knows that means “fast enough for intended use”, not “fast in an absolute sense”. But for some reason when Rust describes itself as safe people take that to mean in an absolute sense.
Or more likely, an error in the formalization. "What you proved is true, but it's not sufficient for what you care about." See for example WPA2 KRACK attacks after WPA2 was proven secure.
This moving of goal posts whenever correctness through type systems is being discussed is a bit tiresome, because it quickly leads to such ad absurdum corner cases.
Yes, you are all correct. The compiler may have a bug. And if it does net, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.
But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.
And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?
Oh, I think you're so right. I heard ton of people online assuming that Rust could help to catch any freaking bug, and when they noticed that - well, it obviously doesn't - ah, then it's just crap or hype.
In theory it would be possible to formally verify the soundness of the borrow checker. Maybe with AI advances we'll be able to do that in the near future. I mean, how much more complicated can it really be than proving Navier-Stokes?
Interesting, the main argument is that C need too much expertise of programmer to avoid problems.
Now, you have a language sold as safe, with popularity made manily blaming C... but now we can say it gave the false sense of safety, distracting programmers from real issues in the name of its error messages that lead for endless refactoring if some new feature is added to project just to o have peace with the compiler. It is a language that program the programmer, an inversion of roles.
> but now we can say it gave the false sense of safety
Except we can't say that, at all. This is just a single bug in relatively obscure code, so 99.99999% of your code remains safe.
Meanwhile in C, 100% of your code has the potential to trigger a similar bug, except there's no path for the underlying cause to ever be fixed, unlike here.
You're essentially complaining that something isn't 100% safe, but that's just your misconception of what "safe" means. Nothing is 100% safe, not can it ever be.
It's especially ridiculous to then compare something 99.999% safe to something 0% safe and conclude that all that "supposed safety" is useless, because look: in 0.001% of cases it's NOT safe!
Both the "100% of of your code has the potential to trigger a similar bug" and "there's no path for the underlying cause to ever be fixed" are just nonsense.
Considering this has gone unflagged for 11 years... Finding a flaw in Rust’s safety guarantees doesn’t mean that they provide no benefit, over a programming language without them.
>but now we can say it gave the false sense of safety
Ok, but that perspective is only valid from Rust++ users who get to mog both Rust and C users. It's not a valid perspective from C users.
Also, your position against Rust is really strange to me, because I love the lack of mutable aliasing. If you think it is a punishment for the programmer you're stuck in a programming model from the 70s. Rust's model is theoretically optimal both from a hardware design perspective and a compiler perspective.
VLIW compilers love Rust because the lack of mutable aliasing by default allows aggressive instruction reordering and instruction level parallelism! Software managed caches are only possible by essentially dragging the cache coherency protocol into the software level!
The sad news is that LLVM is a classic compiler backend optimized for mutable aliasing, which means it is not that great at producing code for VLIW architectures.
> It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against.
Note that Rust is not a theorem prover and Rust programs are usually not formally verified (there are some extensions like Creusot to verify Rust programs, but they are incomplete and a work in progress)
Compiler bugs are, like, just logic bugs. There's a project to eliminate compiler bugs that cause unsoundness, project zero [0] but, still, without formally verifying the implementation, there is nothing really guaranteeing there's no such bugs left.
(note: unsoundness in this context means having safe code cause UB due to a compiler bug; the fix is usually to make the compiler reject the code with a compiler error)
To make matters worse, Rust still doesn't have a spec, and there is not even a tight definition of what are the rules of unsafe code - that is, what rules you must follow so that you unsafe code doesn't trigger UB. Discussions around this are done mainly in issues of the unsafe code guidelines repo [1]
Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.
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.
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.
Sure if you ignore the most popular desktop OS in the world.
Also overcommit (at least how Linux does it) is dumb. It leads to broken OOM behaviour (killing a totally random process, or more often locking up the system and hard rebooting). And some apps do need to handle OOM properly, e.g. formal verification systems which can use enormous amounts of memory. Jasper has to resort to monitoring page fault stats to know when it is using too much memory.
no it doesn't. the broken oom behavior is distros not configuring earlyoom/systemd-oom properly. The problem here is that the kernel doesn't know what software is critical to your OS so the distro needs to be responsible for what processes to protect.
For apps that need to handle oom, Linux is missing something a handle to tell apps to shrink their memory use. Apple does this and it seems to work quite well (and proves that Linux style overcommit works well since it's what they use)
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
On a typical Linux box, overcommit and eager or confused OOM killer will ruin your day anyway.
For no_std style work where running out of memory is actually a hard limit, you have two choices:
1. disable the global allocator and use APIs that take Allocator, to force yourself to only consume APIs that can return errors from allocation. (The ergonomics aren't always great, and fattening all types with a pointer to Allocator isn't great; might be able to use a zero-sized Allocator, with trickery. Say goodbye to many libraries.)
2. use static analysis and try to avoid ever hitting a code path like Vec::with_capacity that doesn't return a Result. Make sure the tooling also analyses your dependencies. (Tooling for the static analysis is painful. And still, say goodbye to many libraries.)
I do wish there were more conveniences for alloc-can-fail APIs, like the failable version of Vec::push needs both try_reserve and push_within_capacity (nightly only).
As much as I would love this on principle, I don't think Rust can make it ergonomic without huge changes like bolting on algebraic effects or something.
I you trust Rust you're trusting clowns like this [https://www.youtube.com/watch?v=E7RJIwEdV5g] compiler team co-lead, or the other co-lead Wesley Wiser, who has never been seen speaking in public. Not to mention the Rust Foundation CEO [https://www.youtube.com/watch?v=O7SwRs0j_Zo] who sits somewhere in Wales and seems to have zero qualifications besides coming from an NGO sponsored by NED, the CIA front end.
It all smells like a US government project with random clowns performing on stage.
Hey, but it's genuinely a nice language. Maybe they're not the most brilliant of type theorists, but even without ownership/borrowing, just stuff like traits, structs/enums/unions with pattern matching, etc, is done quite well.
On HN it's unacceptable to attack or mock people, or make baseless accusations of being shills or stooges like this. It's not what HN is for and destroys what it is for. Please take some time to read the guidelines and make an effort to observe them if you want to participate here. https://news.ycombinator.com/newsguidelines.html
The Rust compiler (rustc) is written in Rust, but there can always be bugs in the compiler, regardless of whether it's written in a memory-safe language or not.
319 comments
[ 1.5 ms ] story [ 21.4 ms ] threadThe fact that nobody reported this before means it's not, by definition.
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.
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.
The age of software means bugs are more likely to be discovered but not necessarily fixed. In the case of Rust, the developers have documented a whole lot of unsoundness bugs that require a new borrow checker architecture to fix.
When implementing the type system, however, variance does have to be treated with care. Historically it wasn't much, now it is.
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).
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).
Also, the Q_free function should not free q->t. It may access it (e.g. printing it), but it does not own that reference and is not responsible for deallocating its memory.
Sorry, I should have looked closer the first time! My excuse is that it was too early in the morning to be thinking about such things.
> Also, the Q_free function should not free q->t.
Well, that's because I thought it would own it. But if in Rust it is not implied that the Q owns the string, then I fail to see where the error is? Both l and q will be deallocated at the end of the main function. Depending on the order of the deallocation maybe q exists for a theoretical time while pointing to already deallocated memory. But both get deallocated at the same point, so q does not outlive the existence of l, so where is the error?
Why?
The issue is that the destructor of q can observe a reference which is about to be deallocated as having a 'static lifetime (i.e. it will live forever), and can thus stash it away somewhere for other code to access after it's been freed (as in the examples in the issue which demonstrate UB.)
I doubt my read is fully accurate, there's probably a relatively small niche where it occurs. But it does seem to be a rather glaring gap, for how long it has existed.
(All languages have this, this is not a rust bashing. Rust seems to do quite well for how complex it is)
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.
https://github.com/rust-lang/rust/issues/25860
"Serious" soundness bugs? That's a stronger claim, and one that you introduced. So you have the burden of proof. Which of those soundness bugs are serious, and what about them makes them so?
> How on earth was this not found before this???
https://github.com/rust-lang/rust/issues/164250#issuecomment...
> Assigning P-high
https://github.com/rust-lang/rust/issues/164250#issuecomment...
In general I agree with fg137's assessment of soundness bugs as being inherently high-impact, i.e., serious:
> The Rust community is well aware that such bugs exist, will be found, and address them just like other high impact bugs.
This is not even the first soundness bug that appeared on HN frontpage. It just means you don't pay attention to Rust development, that's it. I don't even use Rust at all yet I know a number of quirks about its compiler.
This is not a counterargument to my claim that "#1 on HN" status implies that many people are surprised by this.
> It just means you don't pay attention to Rust development
Correct, I don't. I never said that I did.
I hereby confirm that you are 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.
Hope that settles this meaningless exchange.
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.
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.
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.
Sweet. But why should anyone care..
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.
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.
“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.
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.
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...
- 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 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.
- 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
Can you provide an example of such a program that can’t be fixed at the program level like a C++ example?
Not really: the program still needs to be fixed, but fixing the compiler ensures that this unsound behavior never happens again for everyone.
For what it's worth, Rust fanboys also seem just a vulnerable to their ignorance of C/C++ compiler extensions and tooling (e.g. sanitizers, compiler extensions, standard library hardening modes and so on.) which are just normal part of professional C/C++ use today.
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.
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?
> 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.
PS: The term you are looking for is formally verified not mathematically proven.
`sum(a:int, b:int)`
not guaranteed ANYTHING.
The gulf between how much correct Rust is and the vas majority of languages is HUGE.
That's why I specified python 2. No type annotations at all.
It is moral though, so who cares really.
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.
[0] https://safecpp.org/draft.html
The real short coming it is very common for people to not write modern C++. I know several C++ developers who refuse to use smart pointers because they don't like magic happening.
C++ has a terrible reputation which is well associated with, say C++98, if you have a good linter you can bop people on the head for using news anywhere outside a few limited locations where you consider it warranted. All working environments have language features or even programming paradigms that are considered detrimental to code ecosystem health and fighting against these is an organizational lift when working in any programming language. Full type security doesn't mean someone can't create an overly generic object and just start breaking code contracts across the code base. C++ has an awful lot of footguns and more warts than most but it can be made to be sane for development and the new language features really bring it on par with other modern languages.
I have worked in C++ (primarily within the Qt framework which pushed hard into const refs instead of pointers) and it's fine. I've also worked in PHP which can also be fine. Rust isn't something I've worked at scale in but it certainly is very attractive if I ever jump to an org working in it - but even in Rust you'll want to restrict style divergence and bad patterns with linting.
These issues will exist for all time. The only question is how rare can we make them.
The obvious follow-up is to find a minimal set of rules that allow us to express what we want without permitting temporal unsafety. The borrow checker is one set of fairly minimal rules that works pretty damn well. Alternatively you could define away the unsafety by giving it semantics, like fil-C does.
It is kind of annoying to use, but at least there is an obvious default choice.
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.
If not, why would they be allowed to do the same in C++
PS: I was very enthusiastic about Cython for a good while and I went deep into it, but I found that it is rather a mess to use in practice. Yes you get C performance within Python, kinda, but you also get all the C footguns, amplified by the complex interactions with Python features.
Yes, you can pass around an object of procedures, but that is awkward, doesn't have any support from the language or stdlib, and from what I can tell isn't a normal thing that is done.
I think you & I are really back & forth-ing "the PLang not enforcing/strongly encouraging a very specific way of doing things that a whole ecosystem/community organizes around". Relying instead on self-organization has many pros & cons, to be sure. Lisp suffered much the same "until" Common Lisp (which still leaves many things open). My tag line lately is: delegation affords so much, but trust sure is tricky. Much of the time people seem to discount the often rather large cost of establishing/maintaining trust. (I'm not saying you are - just that it's an easy thing to do.)
I'd disagree with this point, there is more typing involved with a first draft of code than Python or Typescript, that's certainly true, but if we bring all the tools (e.g. docblock comments for "type declaration") that are habitual to make up for the shortcomings in most developer's minds then that gap shrinks and, imo, ends up swapping. It's cheaper to have automatically enforced and consistently maintained checks than moving that information out of band and the resulting code in a strictly typed and memory enforced language ends up removing a significant cognitive overhead when reading and maintaining the code.
I have a strong aversion to boilerplate code so it's important to try and allow terse expressions when possible - but unstated assumptions are worse than overstated assumptions.
The hand-waving comes from other languages which can’t do anything to prevent their users encounter such bugs and the ensuing CVEs.
But of course Python function were always duck typed so it often didn't matter to the user.
Typing prevents 1 minor bug per developer per year reaching the testing environment.
It costs 2x development time to use. (With LLMs it's doubles token usage, very measurable)
It's not actually a sane trade-off.
I've found type hints to be remarkably useful and catch significantly more bugs than I ever would have thought, and have quickly picked up the practice of using them wherever I code. My general finding is that if I have to struggle to put useful type hints in place, I probably need to rethink my code.
I even type hint my unit tests because I've learned that sometimes type incorrectness means my tests haven't been testing what I thought they were testing.
Frameworks like pydantic[0] can help you turn those type hints into something runtime enforcing too.
[0] https://pydantic.dev/docs/validation/latest/get-started/
As soon as static typing is introduced into a Python code based, the developers start writing unscalable coding patterns that don't scale to larger programs.
Even beyond Python, most gradual type systems are unsound by design.
A few past discussions if anyone is curious:
Counterexamples in type systems (2021) - https://news.ycombinator.com/item?id=48718972 - June 2026 (4 comments)
Counterexamples in Type Systems: programs that crash, segfault or explode (2021) - https://news.ycombinator.com/item?id=36213704 - June 2023 (97 comments)
Counterexamples in Type Systems - https://news.ycombinator.com/item?id=27252899 - May 2021 (62 comments)
[0] https://arxiv.org/abs/2608.28713
So I don't think it's fair to claim that "no-one cared".
Things taking time to fix is not the same as not caring.
Having ideals does not mean there are never bugs.
The eventual formalization of Rust and a creation of a formally proven compiler is presumably going to be the end point of this process.
https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical...
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.
I'm firmly in the "AI is incredibly powerful and useful" camp myself, but there's no question that currently, without good human oversight and feedback, AI output can have many issues which can be described as slop.
But yes, improved type systems are one of the ways this can be managed, and essentially help bootstrap more reliable systems.
There's a minor irony in imperfect system being used to help build more perfect systems, but you could say the same thing about human developers.
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 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.
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.
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.
The truth is LLMs is what you need to be optimising around as they will become the standard.
Nothing is stopping you from enjoying the sort of programming that you like. But I think it's healthy to accept that that style will soon not be mainstream. It will be like knitting your own clothes, and that's okay.
Regarding formal verification, it's not needed, as LLMs already make on average about as many errors as the average human programmer.
For me, 90% of programming is just a tool to get the job done. It's like a machine in a factory that spits out 50 spoons a minute, and it doesn't need to be any more beautiful than that. If you enjoy woodcarving and want to spend an hour making your own spoon, do that and don't let the existence of the machine make you feel that hobby is any less worth loving.
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
If your spacebar heater relies on such behaviour Rust can and will break it. If you're in the crater group you'll be notified and urged to upgrade it.
I think it's a good thing to keep in mind, that the actual implementation of Rust almost certainly isn't sound. Even an "ideal Rust" still has unsafe, which can affect the soundness of even faraway safe code. But I don't think it's nessesarily wrong to talk about Rust as if it were safe. Much of our communication has implicit assumptions, and the way we talk about Rust is no different. It would be exhausting to qualify every discussion of saftey with "assuming the compiler has no bugs", "assuming all unsafe code follows the (not fully specified!) rules", etc.
Ultimately it's like any other implementation of theory into practice. The theoretical model of Rust lets us reason about and design an implementation to achieve certain practical goals even though the model is a simplification of reality. In Rust's case, practical use has demonstrated it achieves design goals like reducing bugs and reducing development time (compared to peers like C++) to a substantial degree.
https://www.python.org/about/
runs everywhere; is friendly & easy to learn; is Open.Yes, you are all correct. The compiler may have a bug. And if it does net, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.
But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.
And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?
There was one in the Linux kernel a while ago that mistakenly eliminated an important null check.
Here's the current list of similar (unsoundness-causing) open compiler bugs in Rust:
https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...
Now, you have a language sold as safe, with popularity made manily blaming C... but now we can say it gave the false sense of safety, distracting programmers from real issues in the name of its error messages that lead for endless refactoring if some new feature is added to project just to o have peace with the compiler. It is a language that program the programmer, an inversion of roles.
Except we can't say that, at all. This is just a single bug in relatively obscure code, so 99.99999% of your code remains safe.
Meanwhile in C, 100% of your code has the potential to trigger a similar bug, except there's no path for the underlying cause to ever be fixed, unlike here.
You're essentially complaining that something isn't 100% safe, but that's just your misconception of what "safe" means. Nothing is 100% safe, not can it ever be.
It's especially ridiculous to then compare something 99.999% safe to something 0% safe and conclude that all that "supposed safety" is useless, because look: in 0.001% of cases it's NOT safe!
Considering this has gone unflagged for 11 years... Finding a flaw in Rust’s safety guarantees doesn’t mean that they provide no benefit, over a programming language without them.
Ok, but that perspective is only valid from Rust++ users who get to mog both Rust and C users. It's not a valid perspective from C users.
Also, your position against Rust is really strange to me, because I love the lack of mutable aliasing. If you think it is a punishment for the programmer you're stuck in a programming model from the 70s. Rust's model is theoretically optimal both from a hardware design perspective and a compiler perspective.
VLIW compilers love Rust because the lack of mutable aliasing by default allows aggressive instruction reordering and instruction level parallelism! Software managed caches are only possible by essentially dragging the cache coherency protocol into the software level!
The sad news is that LLVM is a classic compiler backend optimized for mutable aliasing, which means it is not that great at producing code for VLIW architectures.
Note that Rust is not a theorem prover and Rust programs are usually not formally verified (there are some extensions like Creusot to verify Rust programs, but they are incomplete and a work in progress)
Compiler bugs are, like, just logic bugs. There's a project to eliminate compiler bugs that cause unsoundness, project zero [0] but, still, without formally verifying the implementation, there is nothing really guaranteeing there's no such bugs left.
(note: unsoundness in this context means having safe code cause UB due to a compiler bug; the fix is usually to make the compiler reject the code with a compiler error)
To make matters worse, Rust still doesn't have a spec, and there is not even a tight definition of what are the rules of unsafe code - that is, what rules you must follow so that you unsafe code doesn't trigger UB. Discussions around this are done mainly in issues of the unsafe code guidelines repo [1]
[0] https://goals.rust-lang.org/2026/roadmap-project-zero.html
https://github.com/rust-lang/unsafe-code-guidelines/issues
Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.
The practical upshot to me is that you should be running your rust tests under asan.
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.
Sure if you ignore the most popular desktop OS in the world.
Also overcommit (at least how Linux does it) is dumb. It leads to broken OOM behaviour (killing a totally random process, or more often locking up the system and hard rebooting). And some apps do need to handle OOM properly, e.g. formal verification systems which can use enormous amounts of memory. Jasper has to resort to monitoring page fault stats to know when it is using too much memory.
no it doesn't. the broken oom behavior is distros not configuring earlyoom/systemd-oom properly. The problem here is that the kernel doesn't know what software is critical to your OS so the distro needs to be responsible for what processes to protect.
For apps that need to handle oom, Linux is missing something a handle to tell apps to shrink their memory use. Apple does this and it seems to work quite well (and proves that Linux style overcommit works well since it's what they use)
https://doc.rust-lang.org/std/alloc/trait.Allocator.html
For no_std style work where running out of memory is actually a hard limit, you have two choices:
1. disable the global allocator and use APIs that take Allocator, to force yourself to only consume APIs that can return errors from allocation. (The ergonomics aren't always great, and fattening all types with a pointer to Allocator isn't great; might be able to use a zero-sized Allocator, with trickery. Say goodbye to many libraries.)
2. use static analysis and try to avoid ever hitting a code path like Vec::with_capacity that doesn't return a Result. Make sure the tooling also analyses your dependencies. (Tooling for the static analysis is painful. And still, say goodbye to many libraries.)
I do wish there were more conveniences for alloc-can-fail APIs, like the failable version of Vec::push needs both try_reserve and push_within_capacity (nightly only).
It all smells like a US government project with random clowns performing on stage.