25

My preference is for Coq, but I imagine that others prefer Isabelle. One of the strange things I found about Isabelle is that there is a two-level syntax, where some of your definitions need to be inside double quote. No such nonsense is present in Coq. Ultimately, the one that is most suitable for you may depend on what you want to prove. Both languages ...


18

One thing that I think you'll find interesting is that the "theorem proving" term varies vastly depending on what field you're in. While they are -- in the abstract -- somewhat related, practical theorem proving (like the kind you see elaborated on in the Handbook of Automated Reasoning) has less to do with Coq or Isabelle than you would think. When I ...


15

The categorization in that list is certainly still current. Perhaps one new category has emerged, namely, dependently-typed programming languages. These are essentially automated theorem provers where the primary goal is not proving theorems, but programming. Due to the Curry-Howard correspondence, these two concepts are strongly intertwined. The ultimate ...


15

There is a variety of systems for Interactive Theorem Proving (ITP) -- see also the conference of that name -- Coq, Isabelle, HOLs, ACL2, PVS etc. All of them are relatively challenging to learn, and each has its own specific culture. It is like learning a foreign language: lets say you know English already, and then have the choice of French, German, ...


14

What works If you nest the definition of the fixpoint on lists inside the definition of the fixpoint on trees, the result is well-typed. This is a general principle when you have nested recursion in an inductive type, i.e. when the recursion goes through a constructor like list. Fixpoint size (t : LTree) : nat := let size_l := (fix size_l (l : list LTree)...


14

Validity of higher order formulae is in general not decidable and search spaces are huge, so all you can hope to do is to try to find a proof -- assuming it exists -- by cleverly enumerating the proof space (think sledgehammer, aptly named) but that is rough. Humans can play the oracle, providing the key lemmata to guide proof. Automated provers, on the ...


11

This is a very active research topic, very promising, though full automation of program generation probably has intrinsic limitations (but are human beings any better?). But the idea is still be very useful in assisting considerably the creation of programs by mechanizing many steps, and by automatically checking the correctness of the program generation. ...


11

Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general ...


11

The remark is about one specific usage of Coq, namely formalization of programming language theory. Let us first make clear the distinction between synthetic and analytic: In a synthetic approach to a subject we say that there are things whose basic properties and structure are postulated in one way or another. We then study these things by relying only on ...


10

Here are some nice video Coq tutorials by Andrej Bauer. It's in no way complete, but I think it's a good introduction.


10

The Mizar system is a huge repository of math proofs. See the wikipedia page and the official website. of all of the known mathematical proofs that can be expressed using English statements From wikipedia/Mizar_system#Mizar_language: The distinctive feature of the Mizar language is its readability Proofs are written as articles, of which there are ...


10

Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom to your theory. That being said, there are ways. In Coq for instance, there are various formalisations of the C standard (e.g. Robbert Krebbers' work). ...


9

ProofWiki contains a decent amount of proofs from various areas of mathematics. It is by no means complete, but is a good starting point for what you want.


9

I think you're confusing two things: dependently typed languages are convenient for specifying properties and giving proofs about functional programs. The techniques you mention are possible decision procedures for certain properties of functional programs. The ability to specify program properties usually takes place within a logic. Dependent types are a ...


9

The wag answer: Yes, but at the time of writing, for most nontrivial programs the specifications seem to be just as hard to write and debug as the programs would be. More seriously, babou's answer is good, but I'm also going to suggest checking out the area of dependent types. There's a rather good book using Coq (full disclaimer: written by a friend of ...


9

At first approximation, there is a difference in "locality" of memory access, when a programm just runs forward on the heap in CPS style, instead of the traditional growing and shrinking of stack. Also note that CPS will always need GC to recover your seemingly local data placed on the heap. These observations alone would have been adequate 10 or 20 years ...


8

Proving the correctness of a program in a form of a proof that's nothing but the program itself This is not quite how the Curry-Howard-Correspondence works. First one has to show that the language of choice actually corresponds to some consistent logic. Different languages correspond to different logics, and many languages correspond to inconsistent ...


8

John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation. Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed ...


8

Metamath has a large selection of proofs, built right up from their core in propositional logic. That said, it is painfully lacking in terms of CS theory. Feel free to expand it!


8

Proof assistants such as Isabelle/HOL work on a syntactical level on a logical calculus. Imagine you have the modus ponens rule (MP) $\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$ and the proof goal $\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$ We humans see immediately that this follows with ...


8

In order with the explicit questions: Yes Yes No To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do with programs? That's what the Curry-Howard correspondence tells us. The Curry-Howard correspondence is a relationship between logic and computational models. ...


8

Your reasoning is incorrect. It is true that your hypothetical "proof deriver" cannot derive all true statements. No proof derivation system can, and indeed, it is not even possible to express the set of true statements in arithmetic, which is a consequence of Tarski's theorem on truth, itself a consequence of Gödel's theorem. However, your algorithm does ...


7

I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio: On-board generic automated proof tools: old-school ...


7

This is obviously a problem specific to Coq since I believe there are nicer ways to get around it with some other proof assistants (I'm looking at Agda) At first I thought r was not recognized as structurally smaller because the structure is only about the inductive definition currently handled by Fixpoint: so this is not a LTree subterm even if it is a ...


7

There's nothing stopping you from defining binary numbers in type theory, and this should give greater efficiency in practice. For example: https://coq.inria.fr/library/Coq.Numbers.BinNums.html EDIT: Why not base 10? Comparison on binary numbers can be done in $O(\log_2 n))$ time. If you have base 10, you can do it in $O(\log_{10} n)$ time. But if we ...


7

I would expect a proof assistant to provide: a syntax to express some mathematical statements a syntax to express a proof of one of those statements a computational process to "check" that a proof of a statement is indeed valid (returns success or failure, or maybe does not return at all) Finally, for such a proof assistant to be trustworthy, it should ...


7

From the perspective of Homotopy Type Theory (HoTT), i.e. if we have the Univalence Axiom, there are definitely values of Bool ≡ Bool that are distinct from refl. Because Agda without Axiom K is compatible with univalence, it can't then assume that refl is the only value of type Bool ≡ Bool. ℕ, on the other hand, is an h-set in HoTT (see Section 2.13 of the ...


6

Coq is a bit more cruel than paper proofs: when you write "and we are done" or "clearly" in a paper proof, there is often much more to do to convince Coq. Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here. Several remarks: I used built in datatypes and definitions where I thought it wouldn't hurt ...


6

Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts. The first is the concept of a proof system, which allows you to specify and prove theorems about mathematics or computer science. Dependent types are one elegant way to do this, where the types are the specification language and the ...


6

looks entirely identity function to me, which can definitely be inhabited by a closed term A proof of $\forall C : Prop, C$ is a function from an arbitrary proposition to its proof. Since a proposition isn't a proof, an identity function is not a function from propositions to proofs. The identity function (or rather, a function returning the identity ...


Only top voted, non community-wiki answers of a minimum length are eligible