3 ms·

But you can't determine if a statement is true by simply reading more words. It's also not efficient for doing higher level work. There was a time before we ha

But you can't determine if a statement is true by simply reading more words. It's also not efficient for doing higher level work. There was a time before we had algebra where people were still expressing the same ideas but the notation wasn't there. Mathematics was expressed in "plain language." It's extremely difficult to read for us. For mathematician's of the time there was no other way to explain algorithms or expressions. For simple programs I have no doubt that these tools enable more people to generate code. However it's not going to be helpful for people working on hypervisors, networking stacks, operating systems, distributed databases, cryptography, and the like yet. For that you need a more precise language and an LLM that can reason about semantics and generate understandable proofs: not boilerplate proofs either -- they have to be elegant so that a human reading them can understand the problem as well. We're still a ways from being able to do that.

nextworddev 4y ago
Arguably reading code can’t lead to definitive conclusions about its bug-free-ness
- agentultra 4y ago
  Precisely! And neither can generating a handful of unit tests. As EWD would say, they only prove the existence of one error. Not that there are no errors. If we want more programs that are correct with respect to their specifications we need to write better, precise specifications… not wave our hands around. However for a lot of line-of-business tasks we’re generally fine with ambiguous, informal specifications. We’re not certain our programs are correct with respect to the specifications, if we had written them out formally, but it’s good enough. I think most businesses that are writing software that needs to be reliable and precise are not going to benefit from these kinds of tools for some time.
  - tjr 4y ago
    This is true in aerospace software. Lots of process, lots of specification, lots of verification. I wouldn't want to say that GPT-seque tools would be useless here, but I really don't see them offering the same kind of magic leverage that they might offer on some other projects. And vice-versa! Most software projects do not benefit from the rigor used in aerospace, because it's just not needed, and would be a waste of time. I am definitely seeing ways that GPT tools could speed up some aerospace work, but we need to be really really sure that things are being done correctly... not just mostly correct, or seemingly correct.
- staunton 4y ago
  Reading and proving a spec can though. LLMs are in principle capable of doing that. (If your objection is that the spec might have bugs then "bug free" is subjective and nothing at all can ever lead to definitive conclusions about it)

nextworddev 4y ago

Arguably reading code can’t lead to definitive conclusions about its bug-free-ness

agentultra 4y ago
Precisely! And neither can generating a handful of unit tests. As EWD would say, they only prove the existence of one error. Not that there are no errors. If we want more programs that are correct with respect to their specifications we need to write better, precise specifications… not wave our hands around. However for a lot of line-of-business tasks we’re generally fine with ambiguous, informal specifications. We’re not certain our programs are correct with respect to the specifications, if we had written them out formally, but it’s good enough. I think most businesses that are writing software that needs to be reliable and precise are not going to benefit from these kinds of tools for some time.
- tjr 4y ago
  This is true in aerospace software. Lots of process, lots of specification, lots of verification. I wouldn't want to say that GPT-seque tools would be useless here, but I really don't see them offering the same kind of magic leverage that they might offer on some other projects. And vice-versa! Most software projects do not benefit from the rigor used in aerospace, because it's just not needed, and would be a waste of time. I am definitely seeing ways that GPT tools could speed up some aerospace work, but we need to be really really sure that things are being done correctly... not just mostly correct, or seemingly correct.
staunton 4y ago
Reading and proving a spec can though. LLMs are in principle capable of doing that. (If your objection is that the spec might have bugs then "bug free" is subjective and nothing at all can ever lead to definitive conclusions about it)