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.
Conversation
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
So what I'm thinking is that I might just keep plugging away with the Rust implementation, but not get too fancy with any optimizations and caching - keep things pretty close to the syntax-directed algorithm I've defined.
1
1
Then I'd be wanting to start proving the metatheory of that syntax-directed algorithm. I'd defer more fancy iris stuff to when I want to start pushing for more performance on the implementation.
1
1
Initially the programs should be small (as I'm experimenting), and it'd be easier to get by with less performance. But I would at least have a plan towards better foundations.
1
The main thing I'd be careful about is making sure you have clear separations between the different components for ease of proof. For Coq this is sort of enforced by the way OCaml handles module and in-file dependencies, but in Rust it's easy to have mutually recursive spaghetti.
1
Ah right. It would be pretty handy to have you look at what I'm going at some stage to see if I'm doing anything terrible! I've been keeping normalization separate from checking/inference, for example...
1
But I have experienced Rust spaghetti before and I try to avoid it anyway. 😂
Yeah, I mean, I know you know that, it just starts to actually matter when you want to prove something.
1
1
Nah, it's good to have the reminder. Trying to juggle lots of things in the air and could have dropped that one!