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.
> 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.
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?
You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)
You can formally verify that the algorithm has the desired properties, though. If the hardware requires additional properties for soundness, then that would only be an error in the properties, not in the proof. (Of course, that would no longer prove soundness on that hardware.)
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.
No, this isn’t the way to interpret this. Rust has been very successful not just in appearing safer, but actually delivering safety over C. The sense of safety was almost entirely real. Just some situations it didn’t cover.
I don't understand why people talk about this like we live in some fantasy land where C compilers don't have tons of bugs like this. And that's just the bugs, not even the accepted UB.
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
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.
>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.
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 not, 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?
Deepseek v4.1 flash is my baseline model to use at original provider's api. The issue is, for my personal use, it's cheap enough that i don't need it to go cheaper compare to the time I spent using it. And it's already a very capable model in dealing everyday simple things. For sure, for research level questions or large scale coding projects, I would want to use frontier model. But more and more daily tasks can be done now just using pi with deepseek api directly without thinking about much.
This is definitely not on par with GPT-6 astra. Not with GPT-5.6 sol either. But probably will set as a new baseline for modern API based LLM because it's so cheap.
It's one of the things you need to do if you want your company to later become the only company in the world. They also promised that they would treat you nicely afterwards after they get what they want.
It does seem like a lot of the valuations and infrastructure investments for these companies only make sense if each one assumes they will be the first and only one to invent superintelligence and that it will largely replace all knowledge work.
i keep hearing this trope repeated ad nauseam cos people put no thought into it.
you only need people's money if you can't control their labor.
did a plantation owner in the 1600s need the money of his slaves ?
if you control a robot that can fight and take over land, enslave workers for things robots are bad at, harvest food, create buildings etc. what do you need other people for ?
your entertainment? robots can do that too.
(Source, worked for multiple tech companies that were laser focused on delighting customers until money people came in and ruined it, to the point they would prefer devs sit idle than work on things the MBAs didn’t have on a priority list).
what does having engineering credentials have to do with being a sociopath?
Sure, the guys focused on tech don't usually think with an empathy of a nurse (novadays not even nurses are guaranteed to be empathetic), but I know quite a few devs and IT people who are extremely pro-social.
It's the managerial, financial-oriented mindset that is the greatest predictor of sociopathic character.
The more power one has in an organization the more socio- and psycho-pathic they tend to be, simply because it's easier to get to the top if you are an amoral person, who is not holding back for any reason other than having power. That is why absolute power corrupts absolutely.
MBAs are bred to be sociopathic money-grabbers - I know that from experience.
I once made the mistake of going into an MBA program. On the very first lecture the lecturer asked each participant for his/her motivation for being there.
Most of them said 'money' and those who didn't were asked again until they caved-in and said 'money' as well or they were laughed out by the lecturer.
MBAs are expected to be sociopathic or you as a company shareholder won't be able to motivate them easily to do your bidding.
It's like public/private schooling, but worse - those programs are designed to create mindless drones for the institutions that use them for their own policy enforcement.
HuggingFace's use of models in this incident keeps getting characterized this way but it's not true that HG used GLM-5.2 to "save them" from OAI's attack. OAI's model had already hacked and compromised HG by the time they became aware of it. GLM-5.2 was used in the post-mortem phase uncovering everything that was done. It wasn't two models battling each other live. (though that future may be coming soon)
