Logic & Applications

Logic and applications of logic from @JohnDCook

[Logic & Applications @LogicPractice]

Big logic

https://t.co/PtcxiYt65P

[Logic & Applications @LogicPractice]

In praise of tedious proofs https://t.co/0WGq0xTI8H

[Eric S. Raymond @esrtweet]

I'm here to tell you a dirty secret about Gödel's incompleteness theorems, after having been asked whether we might hit a "Gödel limit" when trying to prove the correctness of computer programs.

My qualification to speak on this is that I'm a software engineer who used to be a mathematician with a strong interest in foundational logic and mathematical philosophy, and I still track the field.

Here's the skinny about Gödel limits...

Gödel's incompleteness theorems are theoretically and philosophically tremendously important, but most mathematicians don't expect the limits implied by those theorems to be important in practice - not at the proof scales accessible by humans.

We don't know for sure, but the intuitive sense of most mathematicians is that true but Gödel-inaccessible theorems are probably far away from us in very weird corners of the space of all formally possible propositions.

The reason for this intuition is that you have to do very odd contortions to construct a proposition that demonstrates Gödel-inaccessibility. Such constructions are not mathematically natural questions.

Consider the contrast with the Continuum Hypothesis or the Axiom of Choice. These arise from very simple and natural questions the answers to which turn out to be unprovable in standard set theory. They are not weird, twisted constructions made specifically to force the axiom system to rupture something.

Because all reasoning about computer programs is reasoning about finite sets, it seems highly unlikely that being able to prove the correctness of a program will ever depend on even unprovable propositions as natural as CH or AC, which are axioms about what you can do with infinite sets.

Still less likely does it seem that the proof of any program will ever depend on a proposition that is Gödel-inaccessible.

So, in practice, it is not worth worrying about Gödel-inaccessibility of program proofs. Unless you're the sort of person who worries compulsively about, oh, I dunno, being beaned by a meteorite made of solid platinum, in which case there probably isn't much I can do to ease your tension.

Of course, we could be wrong. There could be a landmine, or any number of landmines, in the regions of proof space we care about. The real worry about the Riemann hypothesis isn't whether it's true or false, but that it might turn out to be such a landmine.

Then again, the Riemann hypothesis involves claims about infinities. Even if it does turn out to be Gödel-inaccessible (and the most mathematicians don't worry that it is) it would be quite a bit more shocking if a proof on finite sets turned out to be.

[Logic & Applications @LogicPractice]

Extracting Smart Contracts Tested and Verified in Coq https://t.co/SlslvXITkk

[Logic & Applications @LogicPractice]

LaTeX for logicians https://t.co/nBmWuyxCv1

[Logic & Applications @LogicPractice]

Löb’s Theorem and Curry’s Paradox https://t.co/LMWOFRBAW2

[Logic & Applications @LogicPractice]

CPO = complete partial order.

[Logic & Applications @LogicPractice]

Project Everest: Verified Secure Implementations of the HTTPS Ecosystem https://t.co/FcGBYmXGBL

[Logic & Applications @LogicPractice]

The calculus of constructions https://t.co/z2vQx7eRtO [pdf]

[Logic & Applications @LogicPractice]

Intuitionistic logic in Gilbert and Sullivan https://t.co/1nyunOKEkg

[Logic & Applications @LogicPractice]

Agda: a dependently typed functional programming language https://t.co/elmkDoPOo9

[Logic & Applications @LogicPractice]

Lean: open source theorem prover https://t.co/eXlFsAhgRy

[Logic & Applications @LogicPractice]

Primitive recursive functions and enumerable sets https://t.co/bUwwQ2b8L2

[Logic & Applications @LogicPractice]

The completeness and compactness theorems of first-order logic https://t.co/hHishuuhj0

[Logic & Applications @LogicPractice]

Use of Formal Methods at Amazon Web Services https://t.co/lfGdT7KQzx [pdf]

[Logic & Applications @LogicPractice]

The halting problem: You cannot write a program that can tell whether an arbitrary program will complete or run forever.

[Logic & Applications @LogicPractice]

'Every good idea will be discovered twice: once by a logician and once by a computer scientist.' -- @PhilipWadler

[Logic & Applications @LogicPractice]

Fun with combinators https://t.co/FYIWTXFcOI

[Logic & Applications @LogicPractice]

The Algebra of Logic https://t.co/smVxoNzIsK

[Logic & Applications @LogicPractice]

Glivenko's theorem: If φ is a propositional formula, then φ is a classical tautology if and only if ¬ ¬ φ is an intuitionistic tautology.

[Logic & Applications @LogicPractice]

A formal proof of the Kepler conjecture https://t.co/yj9JvXNyRN