The Hoare Cube | Hacker News Reader

The Hoare Cube

johnwickerson.wordpress.com

86 pointsmatt_d23 comments

Open articleView on HN

I'm just glad to know I'm not the only one who finds some of Cousot's writing to be overwhelming.

As will I be to know that about writings about his writing.

I've learned the hard way that logic is one of the most depressing subjects.

(Exhibit 1: No single completely satisfactory form of logical negation)

What do you mean?

Different logical systems use different methods of handling negation. No single system is suitable for all purposes. I'm no expert, but maybe search for information about intuitionistic and paraconsistent logic and how they handle negation.

You could try the OG book of modern logic, to which all 20th century tracts on logic are responses to, Hegel's Science of Logic. Though its very different from what you might expect out of a logic text.

Pedantry: (wrt all) an arbitrary counterexample would be Abramsky, Domain Theory in Logical Form (1991), which is a 20th century tract on logic, but (although they may share a common Limit between them) is also something Other than a response to Hegel.

Its difficult to tease these things out, but Hegel was the dominant philosophical force of the 19th century in the UK, so any logic immediately following that period had to deal with the immensity of his influence. True, once we get to the 90s, its not clear if the authors are entirely aware of the intellectual history and are just building off of ontologies that they have uncritically adopted as "logic," but in broad strokes it is still the case that the development of logic in the 20th century is as a direct response to Hegelian philosophy.

In other words, Nothing called so much of 20th century logic into Being as Hegelian Becoming?

There is no becoming in Hegel

I'd have to read more (or get your clarification?) to understand what you mean; pp82-106* of a translation appear to cover a fair amount of Becoming to me?

https://archive.org/details/georg-wilhelm-friedrich-hegel-sc...

* including subheads such as "Moments of Becoming" and "Sublation of Becoming".

(ok, reading pp106-108 suggests that although Becoming is not Nothing for Hegel, it is self-contradictory and hence a special kind of a non-being, a determinate being?)

EDIT: aufheben seems more transparent than "sublation"

> Das Werden ist das Verschwinden von Seyn in Nichts, und von Nichts in Seyn, ... Es widerspricht sich also in sich selbst, ... eine solche Vereinigung aber zerstört sich. Dieß Resultat ist das Verschwundenseyn, aber nicht als Nichts; ... Das Werden so Übergehen in die Einheit des Seyns und Nichts, ... ist das Daseyn.

(Becoming is the disappearance of Being in Nothing, and of Nothing in Being, ... It contradicts itself ... such a union destroys itself. This result is the disappearance, but not into Nothing ... Becoming, passing thus into the unity of Being and Nothing, ... is Existence.) ??

https://www.gutenberg.org/cache/epub/6729/pg6729-images.html...

You should start with the Phenomenology of Spirit

My advisor used to go drinking with the Cousots'. He said Cousot becomes more scrutable with more wine. I asked my advisor if he meant Cousots' papers or Cousots' conversation; his answer was "more French".

Can someone ELI5 this, please?

The traditional Hoare logic is the "partial correctness" form - if the program state satisfies a precondition, and executing the program terminates with some other state, then the second state satisfies the postcondition. This is "correctness" in the sense it overapproximates all executions: if the postcondition says something about the state being "good", the precondition ensures you end in a "good" state, but perhaps there are more "good" states than actually reachable ones. It's partial because nothing is said about non-terminating executions.

A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state.

The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.

I would never make a moral judgement on a cube.

Reply on news.ycombinator.com