| > AI will replace humans because giant business believe they can do the same work, not because they will actually be able to. This has been being claimed for at least 2 years now. Wouldn't we already be seeing disasters if this was the case? It's certainly been around long enough to cause some real damage. Instead there is a slow trickle of things that makes the news by people who didn't bother instituting a single fucking control. For example, I am completely immune to `rm -rf` style fuckups because I wrote rm-safe years ago and it is mapped to `rm` in any environment that the LLM will run in: https://github.com/pmarreck/rm_safe In any event, it's not a replacer, it's an augmenter. Nothing will replace humans, because we are the stakeholders; it may shift them around, though. > The correctness of an application is limited by your ability to understand and describe what you need. If you write code in Lean 4 or Idris 2, you may not completely understand why it is or isn't correct, but their respective compilers will certainly prove it to you one way or the other. We already are perfectly functional with incomplete understandings. An entire generation of web developers have had successful careers without having a single clue how compilers work or how machine code works. Now is there a type of problem that sometimes comes along that DOES require deep understanding? Of course, that's when you call in the heavy artillery. Or the advanced LLM. Or both. See my point? |
No, the prover can only prove that the implementation matches the formal language specification. That's different from the application being correct.