>It's conceivable that in an alternate universe an individual engineer's productivity could be so high, because of math, that one developer would replace a whole team from our universe, and bugs would be extremely rare and mostly restricted to UI.
I think this only applies for strictly theoretical problems and code golf, but not in real world programming. It's likely useful for low-level servers like compilers and parsers, but most of the world isn't working on those problems.
For any engineering task (not just software engineering) half of the problem is modeling the problem. Most bugs I see in systems by non-junior engineers are in this camp; the engineer thought one thing but the world was actually different (and this abstracts up to, where management thought one thing, but the world was different).
For a parser, that problem is easily defined. For other problems, the difficulty of programming just moves into verifier. Even if your code was bug-free, it isn't the case that your verifier is. For example lets say you are building a search engine; how do you embed the fact that queries for "Justin Beiber" should rank higher than "Justin Timberlake" except for when the term "super bowl" in included? Or how does the verifier embed the fact that local government regulation says that queries for "Winnie the pooh" should only return results for the kids cartoon character? Finally, Godel's shows us every system will have useful results that cannot be formally verified.
On a more human level, I think verifiers have great use in building more stable systems but I don't think we will see a day where they make us more efficient. It's like believing cars will lead to people staying home all day just because it will only take 5 minutes to get to the grocery store. No, the human mind will invent evermore complex systems on top of the tools we have requiring even more engineers to manage them.
> For any engineering task (not just software engineering) half of the problem is modeling the problem. Most bugs I see in systems by non-junior engineers are in this camp; the engineer thought one thing but the world was actually different (and this abstracts up to, where management thought one thing, but the world was different).
What burns me just as often is when "the problem is modeling the problem" garners a response of refusing to model anything, lest ye be wrong. This is the realm of architectural astronauts that have not yet accepted that title. I'll just put some mechanism in here where the user can make this code do whatever they want and all will be good.
This is sabotage masquerading as reason. As a somewhat senior person, refusing to decide is leaving that decision to your 'inferiors', who then bear the shame of having guessed wrong. Their track record looks worse, and yours looks better. See, you can't trust they new guys with anything. They always fuck it up. That's why you should listen to me instead.
I'm getting real tired of working with Grima Wormtongue.
What I expect from senior devs is that they have a plan, and one or more backup plans. When Plan A doesn't work, I expect them to acknowledge it and flip to Plan B. I get disappointed a lot, and I can see it in others as well. I can't tell you how many times I've surprised someone into stunned silence by practicing what I preach. Wait you're not going to fight me about how your plan didn't work? What is happening?
I think this only applies for strictly theoretical problems and code golf, but not in real world programming. It's likely useful for low-level servers like compilers and parsers, but most of the world isn't working on those problems.
For any engineering task (not just software engineering) half of the problem is modeling the problem. Most bugs I see in systems by non-junior engineers are in this camp; the engineer thought one thing but the world was actually different (and this abstracts up to, where management thought one thing, but the world was different).
For a parser, that problem is easily defined. For other problems, the difficulty of programming just moves into verifier. Even if your code was bug-free, it isn't the case that your verifier is. For example lets say you are building a search engine; how do you embed the fact that queries for "Justin Beiber" should rank higher than "Justin Timberlake" except for when the term "super bowl" in included? Or how does the verifier embed the fact that local government regulation says that queries for "Winnie the pooh" should only return results for the kids cartoon character? Finally, Godel's shows us every system will have useful results that cannot be formally verified.
On a more human level, I think verifiers have great use in building more stable systems but I don't think we will see a day where they make us more efficient. It's like believing cars will lead to people staying home all day just because it will only take 5 minutes to get to the grocery store. No, the human mind will invent evermore complex systems on top of the tools we have requiring even more engineers to manage them.