Hacker News Reader

Comment by fassssst | Hacker News Reader

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.

View on HN

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.

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.

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

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.

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.

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.

> 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?

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.

What kind of verification is done without a formal system?

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.

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.

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.

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.

Would the point not stand if they had said ML or Prolog?

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.

    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_stoc...)

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!

    Imagine if software with large inherent risk was developed using formal
    methods, and the massive remainder of software was developed using rapid
    development methods.

Imagine if we could tell the difference between use-cases with large inherent risk and the massive remainder of use-cases and avoid using software designed for low-risk situations in high-risk applications.

I have worked with systems written primarily in SQL, a declarative language, and I can't say a domain experts could have contributed anymore or less than when I have worked with systems written in Ruby or Java.

Reply on news.ycombinator.com