Comment by lambdaone
11 days ago
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.
Why would that be ironic? AI is helping us find so many subtle bugs and isolate the root cause, it’s nearly perfect for this type of use case.
Perhaps they meant "like an iron, it will stamp out the bugs"
Until they find bugs in the formal proof program ;)
https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical...
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.
[dead]
The UB goes all the way down!
> complete reliability.
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
That’s why they said “closer”
Just wait until someone relies on that bug too.
Rust considers fix to unsoundness bug, a change that can be done at any SemVer revision (i.e. a patch version bump can break it).
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.
What aspects of it are remotely ironic?
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”
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.
4 replies →
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 browse Hacker News stories via this: https://unslop.news/
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.
Yeah the HN home page today seems especially bad
Wow interesting
Reddit r/programming banned AI topics and AI written content and comments. Unfortunately there is not a whole lot going on there anymore as a result.
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.
9 replies →
Thank you for citing the Anthropic propaganda manual!
lobste.rs has a `vibecoding` tag that you can hide.
I didn't realize that, thanks
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.
and what stops AI from "accidentally" writing code with such bugs?
Code review and testing? As always?
[flagged]
1 reply →
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.
Or we realize that it is not possible, and Rust accepts to be "just" a definitely safer C.
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
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.
4 replies →
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.
Because people want a performant optimizing compiler.
5 replies →