1. 2

    i think there’s a confusion here – curry-howard is a statement about running programs as proofs, not about programs as such as proofs. of course we can’t have a programming language that expresses first-order logic at the syntactic level; the compilation of the program would be undecidable.

    1. 6

      we can’t have a programming language that expresses first-order logic at the syntactic level; the compilation of the program would be undecidable.

      We have heaps of languages whose complication is undecidable! Any language with macros. C++ templates. Java generics. TypeScript’s Type system …

      1. 1

        Is it? my understanding is that it’s “the program is a proof of its type”, not “running this program gives you a witness” kind of thing (like reflection in Coq could give you).

        There are languages designed for writing verified code, like Dafny or Why3, and they do embed first-order logic; simply it’s in separate code annotations that express Hoare-logic invariants. Compilation remains decidable, but verification/proving is obviously not.

      1. 8

        UPDATE: paper is possibly being withdrawn due to an error, sounds like in Theorem 1 on page 7.

        1. 4

          Withdrawl is now on arXiv: “Paper is withdrawn because a counterexample was found to Theorem 1”.

          1. 1

            PDF is not on arXiv since it’s been withdrawn. Anyone still have it? Or (inclusive or) details on the counterexample?

            1. 4

              You can access previous versions on arXiv. Try https://arxiv.org/abs/2008.00601v1.