Then separately, you might design a language in Iris whose semantics were those of the abstract machine, and try to prove them observationally equivalent (using some sort of contextual refinement, maybe?).
Conversation
Tbh this is going a bit over my head. Why would imperative semantics be useful here? Is it because it might lead to a more efficient implementation?
1
Well, they're what you're actually *implementing*, so if you want to tie this proof to what you're doing it's necessary. You don't have to do it if you just want to prove things about your theory, but in fact most bugs in Coq are not foundational ones, but implementation errors.
1
1
A huge advantage of having parts of the kernel (especially stuff like the reduction machine) formalized would be to catch those bugs, since the correctness of those modules is relied upon heavily elsewhere and they are used all over the place.
2
1
To avoid really bad bugs, you don't need to prove termination (thank goodness--since nobody's proved it for the full CiC with all the goodies anyway), just absence of UB. That's why I recommend using something like Iris, it is good at such things, e.g. iris-project.org/pdfs/2017-esop.
1
1
What do I do once I have the Iris thingy? Do I extract an implementation from it? Or do I write it separately and try to ensure it matches closely?
2
Ideally you'd extract an implementation, but in practice we aren't really there yet, so you just try to make sure it matches closely. It's not a satisfying answer and I hope to improve that! That said, I believe even something like that would catch almost all implementation bugs.
1
1
Understandable! But it would be a whole lot closer than a ton of other systems!
2
1
I kind of also want to be able to use this in the shorter term in Rust programs, but I think later on I'd want to be able to compile it as a standalone thing. So ease of use as an embeddable language might demand it be written in Rust in the short term.
1
I think Rust is a quite good choice for implementing a dependent type checker (tracing GC would be nice in a few places though). In any case, the "efficient typecheckers tend to have opaque implementations" issue would most likely be true even of a purely functional version.
1
What worries me about Rust is its complexity, and whether implementation bugs could sneak in from the side. Kind of my crazy, overly ambitious ideas with Pikelet was to try to avoid some of those pitfalls. But the more I know the less I know! 😬
Rust programs (or at least, their lambda-Rust equivalents) are actually quite modular to prove stuff about, because it has its own semantic soundness theorem, and ownership provides such strong semantic guarantees (in a way that manifests in Iris since it is a separation logic).
1
1
You can still have bugs from stuff like trait lookup resolution not being what you expect, of course (something we still need to model) but for an imperative language it's not bad. Especially the safe fragment.
2