Re:Small functions considered harmful
by agentultra on Friday August 11, 2017 @11:28AM
(#14990635)
Thank you for posting this.
We see this a fair bit in formal methods of software construction. I can write a specification that proves that given a precondition a particular state will eventually result in a consequent state. The model is mathematically sound but it doesn't state when that transition will occur or how long it will take. And for the purposes of the specification it is likely not important!
The level of detail that is important should be deliberately chosen. A specification of a distributed system can choose to abstract away the details of the TCP protocol while still proving that the properties we do care about, consistency perhaps, are maintained.
We see this a fair bit in formal methods of software construction. I can write a specification that proves that given a precondition a particular state will eventually result in a consequent state. The model is mathematically sound but it doesn't state when that transition will occur or how long it will take. And for the purposes of the specification it is likely not important!
The level of detail that is important should be deliberately chosen. A specification of a distributed system can choose to abstract away the details of the TCP protocol while still proving that the properties we do care about, consistency perhaps, are maintained.