6 ms·

Well maybe instead we'll spend our time honing the spec and doing lots of testing instead of mechanically writing and reviewing code. I see that as potentially

Well maybe instead we'll spend our time honing the spec and doing lots of testing instead of mechanically writing and reviewing code. I see that as potentially a massive net positive for software quality.

marcosdumay 4y ago
You mean honing the spec enough so that it is unambiguous? Maybe you can use some special purpose artificial language created with the purpose of writing unambiguous texts... Like Java or Python.
- fassssst 4y ago
  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.
- CuriouslyC 4y ago
  The fatal flaw in your sarcasm is that specs are declarative but those languages are imperative. Those languages also have more syntax than is strictly necessary, which limits the ability of domain experts to contribute to the spec without the assistance of a developer.
  - kristiandupont 4y ago
    Would the point not stand if they had said ML or Prolog?
    - CuriouslyC 4y ago
      There would still be the point of requiring knowledge of an arcane syntax that can take months to understand and years to master. It will almost always be more efficient and productive to specify programs in plain English then add additional specifications to clarify ambiguity when observed, rather than trying to write specs in a completely unambiguous language.
      - quanticle 4y ago
        then add additional specifications to clarify ambiguity when observed That's such a clean, almost clinical way to describe, "After the software has caused several billion dollars in trading losses, bankrupting the entire company." (https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stock_trading_disruption https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stoc...)
        CuriouslyC 4y ago
        Imagine if software with large inherent risk was developed using formal methods, and the massive remainder of software was developed using rapid development methods. It's almost like there are different tools, and they can be applied to different jobs to cause improved outcomes based on the overlap between the tool's properties and the job's properties. What a radical concept!
deleted 4y ago
[deleted]

marcosdumay 4y ago

You mean honing the spec enough so that it is unambiguous? Maybe you can use some special purpose artificial language created with the purpose of writing unambiguous texts... Like Java or Python.

fassssst 4y ago
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.
CuriouslyC 4y ago
The fatal flaw in your sarcasm is that specs are declarative but those languages are imperative. Those languages also have more syntax than is strictly necessary, which limits the ability of domain experts to contribute to the spec without the assistance of a developer.
- kristiandupont 4y ago
  Would the point not stand if they had said ML or Prolog?
  - CuriouslyC 4y ago
    There would still be the point of requiring knowledge of an arcane syntax that can take months to understand and years to master. It will almost always be more efficient and productive to specify programs in plain English then add additional specifications to clarify ambiguity when observed, rather than trying to write specs in a completely unambiguous language.
    - quanticle 4y ago
      then add additional specifications to clarify ambiguity when observed That's such a clean, almost clinical way to describe, "After the software has caused several billion dollars in trading losses, bankrupting the entire company." (https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stock_trading_disruption https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stoc...)
      - CuriouslyC 4y ago
        Imagine if software with large inherent risk was developed using formal methods, and the massive remainder of software was developed using rapid development methods. It's almost like there are different tools, and they can be applied to different jobs to cause improved outcomes based on the overlap between the tool's properties and the job's properties. What a radical concept!

deleted 4y ago

[deleted]