4 ms·

I was struggling to find the word, but I think I do mean "declarative." It's also deductive, but I'm looking at it from the point of view of what I'd have to do

by bulatb 2y ago

I was struggling to find the word, but I think I do mean "declarative." It's also deductive, but I'm looking at it from the point of view of what I'd have to do if I were proving something. I'm on board with testing being formal as in algorithmic. Seems like there's domain-specific terminology (almost wrote "language"!) I'm using accidentally or incorrectly and making a mess. I might have stepped in it with "model." Mainly I just think I see a difference between ways of verifying where the work is doing and the work is being. But it sounds like I don't know enough to have this conversation. Thanks for humoring me, though.

pron 2y ago
It's important to separate how a statement about behaviour is made (e.g. "the program never loses data") and what mechanisms we take to gain confidence that the statement is true, up to, and including proof (i.e. 100% confidence). Such statements can certainly be said to be declarative (as they cannot be executed), but that's separate from how we gain confidence in their validity. To get a sense of why software correctness is often more art than science, consider that an abstract algorithm can be proven correct but real software cannot because a software-based system is ultimately a physical system, and it is not possible to prove that an addition command given to a physical computer will always result in correct addition, even though that is true with high probability. Since confidence can never be 100%, and since many practices -- from testing through formal methods -- have been generally effective at producing software we can trust with our lives, the game is always about balancing confidence with cost. I, for one, believe that TLA+ (and similar tools) can be used in quite a few situations to gain a required level of confidence more cost effectively than other methods, but there is no one right answer to software correctness and trick is learning when to apply different methods.

by bulatb 2y ago

pron 2y ago

It's important to separate how a statement about behaviour is made (e.g. "the program never loses data") and what mechanisms we take to gain confidence that the statement is true, up to, and including proof (i.e. 100% confidence). Such statements can certainly be said to be declarative (as they cannot be executed), but that's separate from how we gain confidence in their validity. To get a sense of why software correctness is often more art than science, consider that an abstract algorithm can be proven correct but real software cannot because a software-based system is ultimately a physical system, and it is not possible to prove that an addition command given to a physical computer will always result in correct addition, even though that is true with high probability. Since confidence can never be 100%, and since many practices -- from testing through formal methods -- have been generally effective at producing software we can trust with our lives, the game is always about balancing confidence with cost. I, for one, believe that TLA+ (and similar tools) can be used in quite a few situations to gain a required level of confidence more cost effectively than other methods, but there is no one right answer to software correctness and trick is learning when to apply different methods.