Comment Be prepared (Score 0) 34
This is why NASA always packs a tin of Bondo with the mission supplies.
This is why NASA always packs a tin of Bondo with the mission supplies.
Formal verification mathematically proves code implements a specification. It does not catch bugs that are specified.
There are entire classes of bugs (logic bugs) that LLMs can find that formal verification literally doesn't even try to.
So you prompt the LLM to "find all the bugs".
Even if the LLM can find every last bug (which in turn assumes that this type of problem isn't NP-hard or has some issue that Godel would point out), just defining to the LLM exactly what a "bug" is seems to be pretty much the same thing as those formal specifications that you just convincingly dismissed as inadequate.
I don't think that there's anything magical about LLMs that would let them get around fundamental mathematical roadblocks.
i had one too, and it was a great medium, and the external drive with both scsi and parallel port made it easy to use on many computers. one of the main uses was sharing files between my pc and amiga, i also took it to work where we had internet (didn't have it at home yet) and loaded it up with all the latest redhat rpm package updates and other new open source software.
My point exactly. With 5 bullets, does a 16% chance of surviving each trigger pull actually mean anything?
It would mean that there's an 83% chance that the rest of us would be spared from more posts expounding on your silly line of reasoning.
The "probability" is meaningless if it is being used to predict the outcome of a single event. Statistics 101.
If that's the case, the next time you play Russian roulette, why don't you go ahead and put in 5 bullets?
Mutually Assured Destruction and even a small arsenal like Israel is said to have makes nuclear war pointless.
If what you say is true, then why is everyone freaking out over the prospect of Iran obtaining nuclear weapons?
From now on, I'm only drinking soda in October.
As long as I pay my electricity, who cares?
Ignoring the fact that you don't seem to know what a laptop battery is, it looks like you could have a promising career as a data center site planner.
Not to mention, blocking more ads and other unnecessary stuff == better performance on the stuff you were actually trying to view. It very likely comes out as a net performance win even with a ~20% disadvantage in raw CPU speed.
If you read this post it shows that AMD stole Intel's design and reverse engineered it.
If you dig deeper, you'll find that AMD originally reverse engineered the *8080*, not the 8086. The two companies had entered into a cross-licensing agreement by 1976. Intel agreed to let AMD second-source the 8086 in order to secure the PC deal with IBM, who insisted on having a second source vendor.
There would have been no Intel success story without AMD to back them up.
(That actually would have been for the best. IBM would probably have selected an non-segmented CPU from somebody else instead of Intel's kludge.)
Even if you use an AI to extract an extremely condensed specification out of the source code, it's hardly clean room if the LLM was pre-trained on the source code any way.
I once worked at a place that had a clean room process to create code compatible with a proprietary product. Anybody who had ever seen the original code or even loaded the original binary into a debugger was not allowed to write any code at all for the cloned product. The clone writers generally worked only off of the specifications and user documentation.
There were a handful of people who were allowed to debug the original to resolve a few questions about low-level compatibility. The only way they were allowed to communicate with the software writers was through written questions and answers that left a clear paper trail, and the answers had to be as terse as possible (usually just yes or no). Everyone knew that these memos were highly likely to be used as evidence in legal proceedings.
I highly doubt that any AI tech bros have ever been this rigorous, and I'd bet that most of these AIs have been trained on the exact same source code that they are cloning.
The only thing stopping you from calling the water pipes in your house "copper-phosphorus pipes" is laziness and poor attention to detail.
Have you ever heard a single person, including plumbing professionals, call them "copper-phosphorus pipes"?
No. Because that's not how the English language works. You're the one who is too lazy and ignorant to figure out how people actually communicate in society.
Hint: The systematization your mind wants to apply to everything is not absolute. You need to figure out when to relax the formal logic rules when they start to result in absurd outcomes.
How much energy are we talking about?
I don't know if it's still strictly true, but they used to say that all of the antimatter that has ever been produced by humans has had enough combined energy to warm up a cup of coffee.
You win this year's Nobel Prize for pedantry.
So according to you, I can't call the water pipes in my house "copper", since 0.05% phosphorus was added to the material to accomodate brazing.
Why does this change make sense? Because you can't plant a flag and wave your dick if you're up there in zero G orbiting a planetoid.
You have to be standing on the surface, and that is what China is on track to do in a few years.
Remember, even if you win the rat race -- you're still a rat.