... and defining precise specifications. I look at requirements as the human-level needs and wants from a system. If we have an intersection of two busy roads

... and defining precise specifications. I look at requirements as the human-level needs and wants from a system. If we have an intersection of two busy roads shared by cars and pedestrians there's an immediate requirement that cars don't run down pedestrians that are trying to cross. We also want to let some cars get through and some pedestrians get through. And everyone should get a chance to get through the intersection. The specification of such a system to meet those requirements is a bit different. We would need to define systems for indication who can cross, when, the timing of various events in the system, etc. It's much more about the technology involved and how it behaves. Now when we get to software we have tools to write precise specifications but they are so often ignored it seems pointless to advocate for them. Developers think they can design a system involving multiple communicating processes and guarantee that no bad state can ever be entered and that good things eventually happen... without specifying any of those properties. Usually they write a hand-waving informal document in a wiki somewhere that everyone forgets about, add some unit tests (if you're lucky) and some integration tests and think reviewing it closely in code review will catch the rest of the, "bugs." It's amazing that this practice has been sufficient in practice for such a large body of software that it almost seems like evidence that formal specifications are not required to write software... and may even be a waste of time! But I think that what we're talking about here is resiliency: we add more hardware when the software doesn't scale well in performance, we add operational tooling when it isn't as reliable as we'd like: but the costs never go down. We add more in order to do more. I don't think we can write efficient software without being precise with our specifications. As Conal Eliot theorizes, we need correctness in order to scale efficiency: proof that we can satisfy certain properties and guarantees with less code; that code we write composes with other systems, etc. Writing less code is the hardest part of building software, in my experience. Update: And think of it this way, if the specification is imprecise then there is no way to determine that a program is incorrect. It could erase all of your data or leak your personal information and that would be perfectly acceptable.