Hacker News

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?

How is this different from any other compiler bug?

There was one in the Linux kernel a while ago that mistakenly eliminated an important null check.

Is this different?

... and even if you formalize it, it could still be false due to an error in the theorem prover itself.

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.

There are no such valid programs. Proof by contradiction:

A valid program would be exploiting undefined behavior in rust, but rust has no undefined behavior. Thus such a program must not exist.

Now a program may appear to work before the fix, but it was never a valid Rust program.

That’s why they said “closer”

Just wait until someone relies on that bug too.

Obviously, many people have viewed AI’s contribution to programming as just producing unreliable garbage.

Yes, that’s an incomplete and tenuous belief, but that’s where the irony is. If you’re omniscient you don’t get to experience irony.

Hey, if Alanis Morissette can make the same mistake…

“Slop generator makes all future programs more reliable”

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.

The UB goes all the way down!

Code review and testing? As always?

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 browse Hacker News stories via this: https://unslop.news/

lobste.rs has a `vibecoding` tag that you can hide.

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.

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

> The unfortunate fact is that a fully sound Python type system would be a pain to use.

Even beyond Python, most gradual type systems are unsound by design.

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.

Yes, until you introduce inconsistent axioms. Then you can prove anything.

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.

Rust’s type system enables the possibility of discovering and fixing a bug like this, and ruling out this class of bugs for all future programs.

The hand-waving comes from other languages which can’t do anything to prevent their users encounter such bugs and the ensuing CVEs.

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

> not even Rust is free from hand waving.

It is moral though, so who cares really.

That's a misunderstanding. This is not a security vulnerability and Rust explicitly does not defend from malicious programs, only from mistakes. This bug however is quite dangerous, because unlike many soundness bugs it seems plausible to hit by mistake.

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

> Most systems these days have over commit

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.

Sure, but it's worth acknowledging that that specific wart is being fixed.

https://doc.rust-lang.org/std/alloc/trait.Allocator.html

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.

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

Ferrocene

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

Afaik loop {} has never been UB, however because llvm started as a c++ compiled where it is, this has been causing miscompilations in rust and C for… nearly two decades (llvm issue 965).

Not at all. There are way more valid lifetimes than the lifetime system of Rust can express. There are countless scenarios where you could accidentally use the unsound behaviour while not producing a segmentation fault because the lifetimes happens to be arranged such that no invalid memory access actually happened.

A program isn't invalid just because it violates the ownership and borrowing rules of Rust. There are tons of programs in the world with shared, mutable access, devoid of Mutexes, Arcs and Locks that nonetheless are completely valid.

That's not how it works. rustc doesn't "check" for specific cases explicitly, the borrow checker (apparently at fault here by reports) has a set of rules that should reject invalid programs. So either one of the fundamental rules was broken (unlikely here from what I've heard), or some optimization caused the rules to not be implemented correctly.

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

That's easily the exception rather than the rule. I've seen custom `Drop` implementations in almost every non-trivial Rust codebase I worked on.

A custom `Drop` appears very quickly with FFI code. Suppose for example you interface with some C library that expects you to call a function to release some resources.

Now we are at the phase where, Rust is “safe” but only if you use it “correctly” and without using X language feature or a custom Y feature.

This is the problem when a language advertises with “guarantees” and it turns out it never had any due to many false assumptions by their promoters.

So what other soundness bugs are there in the language that we need to know about?

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

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

Rust is my favorite language in most domains I program in; I've learned to ignore the online rust OSS community due to a mix of preferring heavy abstractions (then shaming your code if you don't use them), and rude behavior.

This is fine, for the reasons you state: I can use the language and tools while ignoring the jerks.

Have you met humans?

I’d be shocked if people working on and passionate about thing didn’t shit on other thing. That’s natural and even good in moderation. It’s up to a leader to keep it under control.

Yeah Ive actually never seen any Rust team members be toxic. Keep in mind there is a micro niche of tech influencers who try to politicize rust because they associate it with liberalism or something like that and paint Rust community as an opposing force to some status quo they think exists or should exist. Those notions have taken on a life of their own.

People who say this just dont know what they're talking about and are repeating youtubers and X takes.

There's a fanaticism amongst Rust devs that borders on a cult. They even described their thinking as such, unironically.

Even the basic logic is flawed.... That coders can't be trusted to handle pointers, but somehow can be trusted to write "safe" unsafe rust.