Question says it it all, all the time if you add a new variant to an inductive type, or make any minor modification, everything breaks until that modification is reflected else where, is there a way to minimize the effort needed for this kind of modify/experiment style of development ?
Sadly, modularity with respect to changes of inductive types is hard… At least, proof assistants are nice, as they let you know exactly what breaks and where, while with pen and paper you can just throw away your proof and start a new one.
Afaict, the state of the art with respect to modular inductive types is https://dl.acm.org/doi/abs/10.1145/3372885.3373817
Regarding reparation of code, you can look up @Talia Ringer's work, I think she is the expert on the question :)
In the PL world this phenomenon even has a designated nickname, the famous expression problem. AFAIK it's still an open problem although many people came up with very different solutions to the problem. Proof assistants just make the problem harder as they rule out some approaches like e.g. those relying on impredicative encodings.
In the context of dependent types solutions to the expression problem typically end up being some form of datatype-generic programming, e.g. stuff like containers, ornaments and levitation
Having seen some of the solutions outside proof assistants, I must ask: have you seen solutions that you'd actually want to use and are worth the trouble, compared to "just patch the code when needed"? That's not an option if somebody else must be able to write extensions, but that's not part of @walker's stated requirements...
I should say: I considered Scala case classes to be reasonable, but they interfered with exhaustivity checking
In the current state of things it is still somewhat science fiction, but in the context of MetaCoq I think quite a few of us wish we could have something like Coq à la Carte, so that we can play around with a toy subsystem when wanting to test things and not bother about the full-blown system
But yeah, right now the existing solutions are still not quite mature enough… Although I guess the only way to help them become more mature is to get experience with them by trying to use them?
coq ala carte looks really really promising, I watched the presentation couple times and I think I am close to the edge of my personal capability of having to go many times through the proofs of toy subsystems.
Last updated: Oct 04 2023 at 21:01 UTC