Yeah, I've seen it :) No, this is something that wasn't even originally intended to be *possible* in Coq, so no, people aren't screaming urgently for a use case here. You are going to want a module system of some sort, of course, but be careful... dependent types are tricky.
Conversation
Yeah, definitely finding that 😂.
Do wonder if I should at least be starting to model this stuff in a proof system. That's yet another rabbit hole to head down! And from what I hear the proofs can be a pain - lots of mutual recursion and stuff. 😬
1
I think at this point most people involved in Coq development, at least, agree that a majority of the stuff in it should be in a proof assistant (maybe should have been from the beginning). I strongly recommend you try to prove as much as you possibly can; it'll save you later.
1
1
Do you have any recommendations of a proof system? I was messing with Lean for a bit because it worked with VS Code nicely, but they don't have as many libs for TT development atm - like variable binding and such. :/
1
Thankfully I've been writing down my judgements, but it would be nice to have some confidence in the actual metatheory! brendanzab.github.io/pikelet/append
1
One thing I've been toying with (that I should probably actually do) would be to use a tool like Iris to encode the (rough) logic of the reduction machine as an imperative program.
1
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?).
3
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
So you might have two lines of reasoning - one for the foundation, another for the imperative implementation, then you tie those together and ensure that they're consistent?
Yes, precisely. Ideally you show that the imperative reduction machine refines the abstract machine, the imperative typechecker (and positivity one and so on) refine their abstract versions, and a semantic soundness theorem for the abstract term language and type system.
1
1
And that's kind of what you were meaning here:
Quote Tweet
Replying to @awesomeintheory @brendanzab and 2 others
That would essentially be your semantic soundness theorem for the abstract machine language, which is what Iris is designed for. In order to do this, you'd of course also define abstract typing judgements and probably want to link those to your imperative type inference as well.