The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Thank you for your reply Adam. 

It may not formalize all of math, so it's clear that the projects have different goals. 

Is Induction it's own category of semantics? I didn't think so, I thought it was a proof method. But it appears to be the star in Coq. I suppose Coq is actually discrete in that sense; it's a set of type theoretic foundations, and if particular semantics are wanted to be modeled or reasoned about, they could be added within the Coq system. Right? I guess that hadn't been answered, although I'm not sure how to ask for what I'm grasping for; how do the different semantics, axiomatic/operational/denotational/<one other here> interoperate, or are they discrete because it's a fundamental remaining difficulty with the mathematics that has yet to be reconciled?

I did read about three chapters into Software Foundations, but I find that I like having the mechanics of the language explained to me. I found that a lot of times I didn't understand what a particular language item meant and had to go to external sources to resolve the ambiguity. I understand the emphasis is on exercise and use, but it certainly feels much slower to crash on the rocks of what one doesn't know than it is to first understand and then have something to draw from when working through the challenges. I very likely will return to it since I see the current work that I'm doing as more foundational, and SF as a more demanding requirement.

On Tue, May 31, 2016 at 6:57 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

As far as I understand, Coq's foundation is orthogonal to matching logic, which is not nearly strong enough to formalize all of math.  The reduction semantics of Coq (in the definitional equality) can be viewed as an operational semantics, though.  If you want to learn more, you might want to read Software Foundations.

On 05/31/2016 01:20 AM, Kenneth Adam Miller wrote:

So, I was reading a bit about matching logic when I came across "Towards a unified theory of axiomatic and operational semantics", and it gave me pause. There a lot that I think I should understand fundamentally.

What basis does Coq work at, technically? I've read seven chapters into Interactive Theorem Proving and Program Development, and I don't think either axiomatic or operational semantics are mentioned anywhere, because I realized that I didn't know which it utilized. Can someone provide some clarification?

And also, I was pretty curious about the article itself. It purports some interesting ease in the difficulty of proofs. Not to say that I am attracted by a shortcut, but the idea of being able to annotate a language item seemed like a major payoff if proofs can be derived from the concrete implementation and checked against the desired properties. Does anybody have any thoughts or points about Matching Logic? It's a very new idea to me, so I'd like to hear anything that anybody has to say about it. There doesn't seem to be an interactive tool that can be downloaded to familiarize myself with their theory as with Coq though :(