The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

As far as I know, Ynot is a bit more complicated, since it combines this sort of monadic state with axioms that represent constructs which don't exist in Gallina. But that's the basic idea, I think.

On Tue, May 31, 2016 at 4:45 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

You mean like YNot?

On Tue, May 31, 2016 at 2:15 PM, roux cody <cody.roux AT gmail.com> wrote:

To give a brief answer to Thorsten, matching logic (http://www.matching-logic.org/index.php/Matching_Logic) seems to be a "small steps" version of the usual Hoare Logic for proving properties about programs (with state). It seems to be particularly well-suited to prove simple(ish) computational properties of programs with side effects.

Coq, seen as a programing language (sometimes called Gallina) is pure: side effects are not possible (this is even more dramatic than in Haskell, where side effects need to be "hidden" in an IO monad). In effect, a pure language doesn't really need a "program logic": you can directly insert expressions directly into the formulas, and since everything is an _expression_, there's no need for any machinery that handles the extraneous state.

Of course, sometimes we want to represent stateful computations, and there you need some kind of encoding, e.g. along the lines of Haskell's State monad.

On Tue, May 31, 2016 at 1:46 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

Wow!

Thank you so much to all of you.

On May 31, 2016 1:26 PM, "Xavier Leroy" <Xavier.Leroy AT inria.fr> wrote:

On 31/05/16 07:20, Kenneth Adam Miller wrote:
> 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

Just hold tight for a few more chapters!  The chapters Imp, Equiv,
Hoare, Hoare2 and Smallstep explain very well the approach already
mentioned in this thread, namely defining the syntax and (operational or
axiomatic) semantics of a programming language in Coq, and proving
properties about them.

> You can't add a semantics for a language built under and by Coq?

You can certainly define semantics for a programming language in Coq.

> What about Mezzo, there is a language that was built with Coq.

Not really "built with Coq".  Rather, its abstract syntax, operational
semantics and type systems were formalized using Coq, then proved sound.

> If you're right, then I guess that the mezzo source files just map
> down to Coq types eventually.

You could look up the terms "shallow embedding" and "deep embedding"
in the literature.  What you have in mind sounds like a deep embedding
but the Mezzo formalization, and many other P.L. formalizations in
Coq, use the "shallow embedding" approach.

Hope this helps,

- Xavier Leroy