| ▲ | lambdaone 3 hours 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. |
|
| ▲ | stingraycharles 2 hours ago | parent | next [-] |
| 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. |
|
| ▲ | groundzeros2015 44 minutes ago | parent | prev | next [-] |
| > 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 |
|
| ▲ | mi_lk 2 hours ago | parent | prev | next [-] |
| What aspects of it are remotely ironic? |
| |
| ▲ | jere 2 hours ago | parent | next [-] | | 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. | |
| ▲ | brzz 2 hours ago | parent | prev [-] | | Hey, if Alanis Morissette can make the same mistake… |
|
|
| ▲ | bbor 3 hours ago | parent | prev | next [-] |
| Until they find bugs in the formal proof program ;) https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical... |
| |
|
| ▲ | kimi 3 hours ago | parent | prev | next [-] |
| Or we realize that it is not possible, and Rust accepts to be "just" a definitely safer C. |
| |
| ▲ | wongarsu 2 hours ago | parent [-] | | 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 | | |
| ▲ | afdbcreid 2 hours ago | parent | next [-] | | 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. | |
| ▲ | afdbcreid 2 hours ago | parent | prev | next [-] | | 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. | | | |
| ▲ | UncleMeat 2 hours ago | parent | prev [-] | | Because people want a performant optimizing compiler. |
|
|
|
| ▲ | malkia 2 hours ago | parent | prev | next [-] |
| and what stops AI from "accidentally" writing code with such bugs? |
| |
| ▲ | hbn an hour ago | parent [-] | | Code review and testing? As always? | | |
| ▲ | bcjdjsndon 8 minutes ago | parent [-] | | 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 |
|
|
|
| ▲ | lifeisloving 2 hours ago | parent | prev [-] |
| 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. |
| |
| ▲ | streetfighter64 2 hours ago | parent [-] | | 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. | | |
| ▲ | lifeisloving 37 minutes ago | parent [-] | | 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. | | |
| ▲ | SV_BubbleTime 30 minutes ago | parent [-] | | I guess that’s something you need to work through that you’re just so sick of reading about the single biggest evolution in technology since the internet :( Maybe tech isn’t for you if you don’t like trying to stay on top of it. | | |
| ▲ | lifeisloving 13 minutes ago | parent [-] | | Huh... Anyways, I probably know more about llms than you, I probably use them more than you. I just dont want to turn every conversation into a discussion about them. I would argue the smartphone is 1000x more impactful than LLMs, along with many other inventions since the internet. I'm not really sure what contribution llms have had that are actually THAT impactful for peoples lives. Its possibly (but unlikely) a net negative, time will tell. Most people using them are not getting smarter, thats concerning. Most are just making more money for their bosses who are itching to replace them with an llm. |
|
|
|
|
