Just because a problem is NP-complete doesn't mean it's infeasible to produce "good enough" approximate solutions. The traveling salesman problem is a great example of this.
Not only that, the maximum n a dishwasher can hold is small enough that it can be fairly trivially solved within a reasonable amount of time...though to be fair, iterations are pretty slow, but I think that's fairly easily compensated for with axioms (silverware goes in the silverware spot)
It’s an interesting problem to pack the dishwasher with as many objects as possible and maintain the highest level of cleanliness. Sometimes, there’s an small thing leftover so then repack in a different configuration.
my feeling is that stacking a dishwasher involves enough image processing and computer-use (or more realistically robotics) that it's a frontier model job rather than a 'write a program to do it' job
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.
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
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.
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.
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'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 programming for money.
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.
Of course people will still program for the foreseeable future. But it is still a legit question how long it will be before people come to accept a vibe coded program and are ready to deal with its flaws (of course with more vibe coding) compared to hiring a consultancy.
I'm not talking about mission critical software, but bespoke business applications that are produced by software engineering sweatshops and where the actual users are inured to incomplete features with sharp edges, arcane bugs, and incomprehensibly long intervals between bug report and fix.
Even in mission critical software we will likely see a lot of LLM tool usage. Even if the copyright plug is pulled and all vibecoded applications are regarded as copyright violations, its uses to analyze existing code and give advice will remain. In this world, writing applications entirely by hand will become an artisanal discipline.
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.
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.
I think the problem you're seeing is not with LLMs per se, but with capitalism. Imagine we have a quite useful machine that's reducing the amount of work needed to accomplish stuff, and all normal people are afraid of that machine simply because they worry they'll have less work. How backwards is that!
If we didn't let people live off the work of others, as the capitalists do, then we could all rejoice in that we've found yet another way of reducing the labor required to produce stuff.
Yet, in the real world, it seems as despite the progress of technology, the labor of the everyman is constant, and only the richest get more and more shiny jets and yachts.
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.
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.
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.
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.
I wouldn't say so. The gap between GCC and Clang/LLVM is bigger than that on some benchmarks, [0] although the gap between their overall performance (using geometric mean) is much less. [1]
It's a very impressive result considering how much effort has gone into GCC. It highlights how compiler optimisation work can face diminishing returns.
> the norm for releases being O2 if I understand correctly
Agreed, but the difference isn't that great. From the article:
> CompCert code is 7% slower than gcc-01 and 12% slower than gcc-02 on average.
Reminds me of how the cproc/qbe C compiler gets very roughly 50% of the performance of Clang/LLVM in 0.1% the lines-of-code. [2]
Maybe we just have different experiences, but I've experienced a huge amount of friction trying to enable features that cost something resembling 0.5% of fleet performance, even when they provide massive benefits. 12% loss would be laughed out of the room.
I agree that this is an impressive feat. I also don't see why an equivalent for rust would be adopted.
> I've experienced a huge amount of friction trying to enable features that cost something resembling 0.5% of fleet performance, even when they provide massive benefits. 12% loss would be laughed out of the room.
A 12% difference in performance between two compilers, for some given application, is possible even between two of the best optimising compilers available. A 12% performance lag does not necessarily relegate a compiler to obscurity.
The long-entrenched MSVC compiler is still a major player despite that, for at least some applications and for at least some compiler versions, Clang outperforms it by far more than 12%. [0][1]
If a new Rust compiler really could offer significantly fewer compiler bugs, that would of course need to be weighed against any performance penalty, and the proper tradeoff would of course depend on the project.
> I agree that this is an impressive feat. I also don't see why an equivalent for rust would be adopted.
I imagine it wouldn't be widely adopted for most applications. CompCert itself is pretty niche. It's not Free and Open Source software, which I suspect is a factor, alongside its technical drawbacks.
Unless you're working on ultra-low-defect software, such as in a safety-critical domain, compiler bugs are unlikely to be a major factor in your software's quality. If the compiler lacks support for interesting language features, it becomes an even harder sell for 'ordinary' projects that are able to tolerate an ordinary number of compiler bugs.
You can always choose not to reject again if some number of rejections fail. With a sufficiently large random number range, the chances of rejection at any step can be made tiny, and the possibility of successive rejections drops exponentially with the number of rejections allowed until you have a theoretical probability smaller than the probability of hardware bit errors on the platform itself. If this happens, you can either throw once more and use that result, with a tiny amount of modulo bias, or you can just throw an exception.
Oppenheimer, as well as many other Manhattan Project researchers (eg Rabi & Weisskopf), were first or second generation German-Jewish immigrants/refugees. Max Bonn, Oppenheimer’s mentor, was also a refugee in the end; Oppenheimer was born to immigrants in the US but studied under Bonn in Germany prewar.
Moreover, the physical foundation for atomic power was largely the work of German, often German-Jewish, scientists.
So it’s plausible to suppose a counter-factual in which Germany, one less crippled by bigotry (and it is a disability…), develops the bomb.
And it’s not just the bigotry: it’s the anti-intellectualism. Einstein could write a letter to a well-educated patrician of the New York Dutch aristocracy (FDR), and so help change the world. The pig farmer and the corporal would never have read such a letter (even if were they not already trying to murder the writer and all his cousins for nonsense reasons).
OK, they can play chess, but that's not real AI - can they write poems?
OK, they can write poems, but that's not real AI - can they compose music?
OK, they can compose music, but that's not real AI - can they translate languages?
OK, they can translate text, but can they do maths?
OK, they can do maths, but can they solve a Millenium Prize? <-- we are here
"I once knocked a bunch of bananas off a tall man's head. His name is Ash and his leg is like teak. Is he a tree?"
"What? Don't be silly. For one thing, trees have moss."
"OK he's grown moss. He's a tree now right? Right??"
"I doubt it, for I see nothing but wishful thinking to suggest that simulating the appearance of tree characteristics is part of a path to becoming a tree. And that's not actually indistinguishable from moss anyway, is it?"
Imagine meeting a person who could do all of those things.
“I once met a person who could beat any grandmaster in chess, translate any language, and complete international math Olympiad problems. He couldn’t solve any Millenium problems though, so I’d say he was a midwit at best.”
reply