Hacker News new | ask | show | jobs
by thesz 21 days ago

  > As long as the tests pass and the performance doesn't regress...
AMD had 20+ million tests for their FPUs back in the day of Intel's FDIV bug and ACL2 found bugs in their implementations of floating point computation.

Agentic vibe coding is not an application of ACL2 theorem prover to anything. Agentic vibe coding is an opposite of it, it will make its way to pass the tests with any means necessary, be it patching the code, the tests, or expected results.

   > it's secure
You can't say that before formal verification. Which is an opposite of what vibe coding is.