gotchaMinor
The difference between a Hoare Triple/Assertion and a Typed Function
Viewed 0 times
tripletheassertionfunctiondifferencetypedbetweenandhoare
Problem
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.
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.
Solution
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.
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.
Context
StackExchange Computer Science Q#92444, answer score: 4
Revisions (0)
No revisions yet.