I think we're talking at two different levels here. I am not talking about using a sorting routine in a program, but about writing a sorting routine. You want to know that your sorting routine actually sorts. Your routine is a state machine; its blackbox description is a function. You want to prove that your state machine implements the function. Our goal is to verify that mergesort actually sorts. Not that the air traffic control program using mergesort works (we could, but then the ATC program would be the state machine, and sorting would be just a function).
> Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.
This means that both are refinements of the "magical sorting machine". You can use "magical sorting" in another TLA+ spec, or, as in this running example, prove that mergesort is a refinement of "magical sorting". If what you want to specify isn't a mergesort program but an ATC program that uses sorting, of course you'd use "magical sorting" in TLA+. You specify the "what" of the details you don't care about, and the "how" of the details you do.
> I find it a lot more difficult to think about a state machine than about a function.
Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.
> Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.
Well a function is necessarily a function (if we enforce purity and totality at the language level). Presumably what we want to verify is that its output has certain properties, or that certain relations between input and output hold. But that seems like very much the kind of thing we can approach in the same way we'd analyse a mathematical function.
> Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.
This means that both are refinements of the "magical sorting machine". You can use "magical sorting" in another TLA+ spec, or, as in this running example, prove that mergesort is a refinement of "magical sorting". If what you want to specify isn't a mergesort program but an ATC program that uses sorting, of course you'd use "magical sorting" in TLA+. You specify the "what" of the details you don't care about, and the "how" of the details you do.
> I find it a lot more difficult to think about a state machine than about a function.
Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.