If we’re going to continue on this vibe slop timeline, I’d like to see LLM’s start working with formal methods and languages like LEAN4 or Roq to fully test the problem domain in a context that catches logic errors before they’re written. An LLM being supervised by a formally verified compiler can’t hallucinate as easily because the compiler won’t let it most of the time.
If we’re going to continue on this vibe slop timeline, I’d like to see LLM’s start working with formal methods and languages like LEAN4 or Roq to fully test the problem domain in a context that catches logic errors before they’re written. An LLM being supervised by a formally verified compiler can’t hallucinate as easily because the compiler won’t let it most of the time.