4
$\begingroup$

I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function.

That is, say you have a typed function $f : A \to B$. The initial state for the function is thus $A$, and the final state is $B$. Similarly, in Hoare Logic, it would be like $\{A\}\ f\ \{B\}$. It's like the Hoare Triple is a typed function application or something, but I'm sure functional programming has those typed as well.

The types could be complex types such as dependent types that have constraints on the input as well, so you can handle things like $x > y$ and the like. So I'm wondering, what the differences are between Hoare Triples and Typed Functions (in any type system) generally.

$\endgroup$
4
$\begingroup$

You are putting your finger on angular stone of program verification. At a very rough and high level you can think a derivation in Hoare logic as proving a property, thing which can somehow be translated in a type derivation.

More precisely you are almost (you're slightly limiting yourself with Hoare logic) rediscovering the very deep Curry-Howard correspondence with asserts that mathematical proof and type derivation are the same thing.

$\endgroup$
  • $\begingroup$ No I'm saying that a mathematical proof is a typed program and conversely. I don't know about the answers you get about Curry-Howard, but I guess either you misunderstood them, either the are lacking some references in proof theory. A proof (in the mathematical/logical sense) is a well defined object. If you want practical evidence, look at the Feit-Thompson proof in COQ by Gonthier et al: a proof of a Group theoretical theorem done in more than 500 pages as been proven in COQ, that is has literally been translated to a typed program. $\endgroup$ – Sn0w May 29 '18 at 2:28
2
$\begingroup$

To be frank, it much more difficult to see how types and pre-/post-conditions are similar than how they differ.

In Hoare Logic, for the Hoare triple $\{A\}\ f\ \{B\}$, $A$ and $B$ would be predicates on the entire program state and $f$ would be a sequence of instructions, not a function. For example, $A$ might be something like $$\mathtt i = 0\land \mathtt s = 0\land\mathtt n > 0\land\texttt{overflow_flag} = \mathtt{false}$$ and $B$ might be $$\texttt{overflow_flag} = \mathtt{true} \lor (\mathtt i = \mathtt n\land \mathtt s = \mathtt n(\mathtt n+1)/2)$$ You might use this to describe a the pre-conditions and post-conditions of a loop that sums increments $\mathtt i$ up to $\mathtt n$ and has $\mathtt s$ hold the running sum but may set $\texttt{overflow_flag}$ if the numbers get to big at which point there are no guarantees about anything. However, the pre-conditions and post-conditions don't imply this code. Any code that produces the appropriate output (i.e. a program state matching the post-conditions) given the appropriate input (i.e. a program state matching the pre-conditions) would be just as valid. For example, a program that just immediately set $\texttt{overflow_flag}=\mathtt{true}$ or one that just directly set $\mathtt{i := n}$ and $\mathtt{s := n}(\mathtt n+1)/2$. There is nothing in the specification I gave that indicates under what circumstances $\texttt{overflow_flag}$ will be set. Also, unless I'm using some framing convention, there is nothing stated about what happens to all the other variables in the program state. If you want to ensure/know that the other variables were not changed, you have to explicitly state that.

There are many issues with the Hoare Logic approach. It has no real notion of scope, so recursion, higher-order functions, and objects are very difficult to deal with. Also, this makes it very non-modular. For Hoare Logic, in your example $f$ doesn't represent a function, it represents a sequence of instructions. Let's say you have two separate blocks of code proven to meet two separately developed specifications. You'd like to combine both in your program. You can't simply sequentially compose them. If they use the same variable names for different things, you'll need to rename them. You'll need to add framing conditions to state that neither mutates the variables of the other. God help you if you want to do a concurrent composition, because Hoare Logic won't.

Modern descendants of Hoare Logic such as separation logic and Hoare Type Theory address these deficiencies of the original Hoare Logic. ynot, mentioned by Andrej Bauer in a different answer, is based on separation logic.

If it isn't obvious yet, the above is not at all reminiscent of most type systems. Most type systems don't have any way of referring to run-time values in types. Even in most dependently typed systems, top-level types are generally meant to be closed, and certainly they refer to values, not mutable variables. Types usually don't allow arbitrary predicates of first-order logic, and type systems are usually designed not to require proving arbitrary theorems to type check. What you can do, though, and very roughly what ynot does, is make a tuple with all the program state and consider functions $S\times X\to S\times Y$ where $S$ is the type of the tuple of all the program state. You can then consider functions between subset types (perhaps represented by a dependent sum): $\Pi s:S.\{x:X\mid P(s,x)\}\to\{(s',y):S\times Y\mid Q(s,s',y)\}$. A function $f$ of this type would be akin to a Hoare triple $\{P(s,x)\}\ y\, \mathtt{:=}\, f(x)\ \{Q(s_{\text{old}},s,y)\}$. Still, most function types (let alone arbitrary types) are not of this form. Going the other way, terms have types and, in particular, variables are assigned types. There is no analogue in Hoare Logic to assigning a type to a variable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.