Proofs of program correctness are great, but they are too hard for mortals right now. How can I help mortals write and maintain proofs of program correctness?
Conversation
What are the practical engineering implications of what's new and hot in type theory, like cubical? How can I build bridges between type theorists and the folks who work on more PLDI-type work?
1
8
Software engineers and proof engineers hate using new things. How can I take hot new concepts from programming languages and give it to engineers without making them ever switch languages and with minimal tooling overhead, in a way that naturally integrates with their workflows?
2
4
Proofs carry so much beautiful information. What does that information tell us? What can we do with it to make things easier for proof engineers? What are some interesting and useful fundamental truths about the structure of proofs?
1
1
8
How can we infer and automatically prove relations from just datatypes or examples? How can we then use those relations to then update programs and proofs in a way that is guaranteed to preserve them?
1
1
6
As programs and proofs evolve over time, what do those changes tell us, and how can we automate away the pain of that evolution?
1
4
What abstractions do people need to prove the things that matter about their domains? How can we bring verification to new domains? What will this teach us about proof engineering and about programming languages more broadly?
1
3
Dependent types are hard to use. How much of this pain is essential, and how much of this pain is just due to poor automation and tooling? How can we trim away all of the non-essential pain so that we are left with only the essential pain?
1
6
How can we build a good user experience around dependently-typed programming and proving? How can we ask the proof engineer for only the necessary information without prompting the proof engineer for obscure knowledge a tool could just as easily infer?
1
6
That's all for now, but certainly not all in general. Probably useful for anyone who might want me as an advisor at some point. But I'm pretty open-minded. Just observing some themes after a few years of obsessing over this stuff.
2
3
Replying to
This is a bunch of exciting stuff! I'm so glad there are people like you interested in this stuff. The power of first class types and theorem proving deserves to be shared and made more accessible, in my opinion! See also:
Quote Tweet
Replying to @chrisamaphone
I really want to put the power of rich type systems into the hands of more people! To demystify them and help to make them a natural, first-class part of everyday programming. They are a powerful, useful tool and I don't want them to remain obscure!