3 ms·

Those aren't good enough, you really need a formally verified language. Or just use English and do lots of acceptance testing plus add fail safes. I bet that w

Those aren't good enough, you really need a formally verified language. Or just use English and do lots of acceptance testing plus add fail safes. I bet that will be more economical.

gtirloni 4y ago
Look at all the millions of developers proficient in Aqda and Coq.
- naasking 4y ago
  The point is that you don't need millions of developers if AI is writing the code against a spec, you'll maybe only need a few thousand spec writers.
  - gtirloni 4y ago
    I think you're underestimating the number of spec writers. If that ever happens, every company with a custom business stack will need at least a few. That's certainly a few million jobs worldwide.
  - marcosdumay 4y ago
    The point is that if you are trying to replace millions of developers, you will obviously require something on the order of quadrillions of spec writers. Or, rather, this is probably still an underestimation. And yes, it is a very obvious point, and that people keep missing that point on this site is unsettling. (Also, yes, this can be trivially circumvented if you just let those people program, instead of only do verification.) You can, also obviously, replace millions of average developers with (way more) millions of extremely competent spec writers if they can use formal methods. Those will require way more computing power than it can ever exist on Earth to do their work, but they can mathematically get there.
    - naasking 4y ago
      > The point is that if you are trying to replace millions of developers, you will obviously require something on the order of quadrillions of spec writers. Why do you think you need orders of magnitude more spec writers than coders rather than the other way around?
      - marcosdumay 4y ago
        That is an intrinsic feature of software verification. You either have a formal system or you have an exponentially growing amount of corner cases to verify.
        naasking 4y ago
        What kind of verification is done without a formal system?
        marcosdumay 4y ago
        We usually call those "tests", but some people do really like non-formal linter rules too. (Personally, I abhor checking rules with high false positive odds.) AFAIK, those are the only ones in common use, but differently from formal ones, non-formal things tends to come on a multitude of widely different types. So I wouldn't be surprised if people have invented many more.
  - MisterBastahrd 4y ago
    Until your model isn't good enough to generate good code from the best specs you can get. Gonna be really fun when the first financial companies start trying to generate billing software from specs and end up blowing up entire people's bank accounts irrevocably because of lax regulation and greedy shareholders. Not to mention that any resources you trim from the developer side of things you'll have to at least quintuple in QA.
marcosdumay 4y ago
Writing the code with a few checks here or there is almost always sufficient. But yes, if you want to verify the AI's output you better write lots and lots of acceptance tests. Easily pages of tests for each line of code. If the problem is large, it can easily get into millions of lines of test for each line of code. Formally verifying it will easily take more computing power than training the AI on the first place, so I don't count that one as viable.

Those aren't good enough, you really need a formally verified language. Or just use English and do lots of acceptance testing plus add fail safes. I bet that will be more economical.

gtirloni 4y ago

Look at all the millions of developers proficient in Aqda and Coq.

naasking 4y ago
The point is that you don't need millions of developers if AI is writing the code against a spec, you'll maybe only need a few thousand spec writers.
- gtirloni 4y ago
  I think you're underestimating the number of spec writers. If that ever happens, every company with a custom business stack will need at least a few. That's certainly a few million jobs worldwide.
- marcosdumay 4y ago
  The point is that if you are trying to replace millions of developers, you will obviously require something on the order of quadrillions of spec writers. Or, rather, this is probably still an underestimation. And yes, it is a very obvious point, and that people keep missing that point on this site is unsettling. (Also, yes, this can be trivially circumvented if you just let those people program, instead of only do verification.) You can, also obviously, replace millions of average developers with (way more) millions of extremely competent spec writers if they can use formal methods. Those will require way more computing power than it can ever exist on Earth to do their work, but they can mathematically get there.
  - naasking 4y ago
    > The point is that if you are trying to replace millions of developers, you will obviously require something on the order of quadrillions of spec writers. Why do you think you need orders of magnitude more spec writers than coders rather than the other way around?
    - marcosdumay 4y ago
      That is an intrinsic feature of software verification. You either have a formal system or you have an exponentially growing amount of corner cases to verify.
      - naasking 4y ago
        What kind of verification is done without a formal system?
        marcosdumay 4y ago
        We usually call those "tests", but some people do really like non-formal linter rules too. (Personally, I abhor checking rules with high false positive odds.) AFAIK, those are the only ones in common use, but differently from formal ones, non-formal things tends to come on a multitude of widely different types. So I wouldn't be surprised if people have invented many more.
- MisterBastahrd 4y ago
  Until your model isn't good enough to generate good code from the best specs you can get. Gonna be really fun when the first financial companies start trying to generate billing software from specs and end up blowing up entire people's bank accounts irrevocably because of lax regulation and greedy shareholders. Not to mention that any resources you trim from the developer side of things you'll have to at least quintuple in QA.

marcosdumay 4y ago

Writing the code with a few checks here or there is almost always sufficient. But yes, if you want to verify the AI's output you better write lots and lots of acceptance tests. Easily pages of tests for each line of code. If the problem is large, it can easily get into millions of lines of test for each line of code. Formally verifying it will easily take more computing power than training the AI on the first place, so I don't count that one as viable.