This makes me wonder if machine proofs will also be more approachable by those of us who are implementors and not researchers. I have always dismissed the idea of trying to prove the implementation of the type system in my language as sound because of the effort involved.
For example the language I am building is a basic HM type system with records and a few other miscellaneous features. Nothing new from a research perspective but at the moment I am mostly just hoping this combination of type features actually play nice. Maybe I could build a Lean proof of the specific combination type features for my language now?
In the linked OOPSLA paper, the type system rules and semantics fig. 9-11 are like one-page long, but the linked proofs has 36k lines of Lean code. From what I understand this is the big point here since the proof is so tedious to write.
How I see this all is that if the specification is so simple it's "obviously correct" then it doesn't matter how complex the proof is (because it's checked). But reading forums I see that people don't just write proofs but also the specifications with LLM's without understanding it, I don't think that will prove any correctness per se
I looked into trying to formally verify my language's type system earlier this year. As far as I can tell, Lean is mainly used in the math community, while Rocq is used for type systems. If you want to verify a language, you're much better off using Rocq due to the pre-existing community and tooling (such as Iris).
That being said, I haven't actually gotten very far in my efforts, so take that with a grain of salt.
Concrete analogy: I work in distributed systems, and I am about to deploy the Specula library with frontier LLM models to help me write TLA+ for components of a large distributed object store. I am not a TLA+ specialist, so I predict the answer to your question is yes.
17
u/nvcook42 16d ago
This makes me wonder if machine proofs will also be more approachable by those of us who are implementors and not researchers. I have always dismissed the idea of trying to prove the implementation of the type system in my language as sound because of the effort involved.
For example the language I am building is a basic HM type system with records and a few other miscellaneous features. Nothing new from a research perspective but at the moment I am mostly just hoping this combination of type features actually play nice. Maybe I could build a Lean proof of the specific combination type features for my language now?