# Tag Info

### Example of an algorithm that lacks a proof of correctness

Here is an algorithm for the identity function: Input: $n$ Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$ Otherwise, output $n$ Most people suspect ...
Accepted

### Difference between Dependent type , refinement type and Hoare Logic

There is recent work by Paul-André Melliès and Noam Zeilberger that explores this. In particular the papers Functors are Type Refinement Systems and An Isbell Duality Theorem for Type Refinement ...
Accepted

### What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's A Compositional Program Logic for Polymorphic Higher-Order Functions ...

### Example of an algorithm that lacks a proof of correctness

Most algorithms have not been proven correct in Hoare logic. The main reason is that such correctness proofs are extremely expensive as of Jan 2017, probably by several orders of magnitude in ...
Accepted

### Relation between Hoare Type Theory and pointers

A pointer to a variable creates an alias. When the alias is modified, the corresponding variable is modified as well. Therefore, the rule for an assignment in Hoare's logic is not just update the ...

### What is a predicate transformer?

The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition. For example, given a program ...
Accepted

### What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, ...

### Intuitive explanation of Hoare assignment axiom

Hoare Logic proceeds backwards. It is a method to compute a precondition such that the desired postcondition holds. In fact, the inference rules given in your standard Hoare Logic deductions compute ...

Accepted