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.