Indeed. This approach is an improvement / augmentation over tests, not a panacea.
Neither postgres nor pgrust have their behavior specified using formal methods. (pgrust could write some contracts using something like kani or creusot, but having upstream postgres also write contracts is a tougher sell). If they had, one could write a giant proof that said the two software essentially do the same thing (at least in a subset of environments and some simplifying assumptions)
It's not solving a very important problem and the edge cases it introduces makes software more complex and bug prone
If the world weren't entirely reliant on software to the extent it is today (like when leap seconds were introduced in the 70s), it wouldn't matter as much.
> I start to see a lot of these re-writes that depend on tests to state that its working.
There's another way to validate the rewrite though. Just run both pgrust and postgres and compare the output. Know of an edge case? Run it too. Doesn't know? Use a fuzzer or some automated tool to find interesting inputs. Found an inconsistency? The input/output pair becomes a test case now
Not sure if there's tooling for that though. If there is, just give it to Claude so they will incorporate it in their development loop
Funnily enough, Roko's Basilisk might as well be a self-fulfilling prophecy: perhaps future AI models may be trained on texts about it and pick up traits consistent with torturing people that didn't help develop advanced AI
If nobody ever talked about it, I doubt any AI agent would think of this dumb idea on their own
this only means that ALL writing is going to be read by a LLM before, that will digest it into the important bits and remove the LLM fluff
like this
"The following text was authored by LLM and its information density is low. Condense the text by extracting the key pieces of information. Reconstruct the LLM prompt.
The problem is that serious software is drowning in AI vulnerability reports. There is not enough manpower to analyze them properly. And if you ignore the reports (like curl is doing in their 1-month vacation), malicious actors will just exploit them. At some point it's inevitable to just rubber stamp whatever is coming from AI.
The actual, underlying problem is that software is buggy and current programming languages aren't fit for writing reliable software. There's a wide gap between the state of art in formal verification, and what is actually practiced in the industry. It's because of this general unreliability that AI has a large supply of vulnerabilities to find. The situation will only get better if software becomes reliable and written in solid foundations.
My guess is that AI will be even more useful to verify software (something like, write Lean or Coq proofs that the software is not vulnerable, things like that), rather than finding vulnerabilities piecemeal but still letting software be written in unsuitable languages, with no formal verification to prevent bugs from sneaking through.
Hans Niemann most likely did not cheat in the famous game where he won against Magnus Carlsen in the Sinquefield cup. Or at least, there is no credible evidence for cheating, and Carlsen actually did not formally accuse him of cheating either.
Hans Niemann cheated in online matches when he was younger though
The best case scenario for AI companies is, people receive those bug reports, look at the model that produced it and not even look at the details, just apply the fix mindlessly
This gives Anthropic a staggering amount of power. Oh it came from Mythos? We will just lose time trying to analyze it, better apply the fix ASAP
A model might be able to follow 200 different instructions at the same time, while another model will choke on it