> 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?
Re:Software 2.0
by marcosdumay on Tuesday February 21, 2023 @03:51PM
(#34887053)
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?
Re:Software 2.0
by marcosdumay on Tuesday February 21, 2023 @04:29PM
(#34887686)
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.
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.