We're building up a sizable array of highly complex proofs; cf. rejection sampling for example.
If a customer wants to understand what we are even proving by looking at the .ML themselves, they sometimes have to dig through >1000 LOC before finding the core theorems, and then they're not always marked as such or documented in detail.
We should consider introducing separate files for just the core theorems that we want the user to vet. It also makes review a bit easier, because we, too, should be content -- trusting the HOL-Light TCB -- to judge a proof contribution primarily based on its spec (primarily because there's also performance and maintainability concern, of course).
RFC @mkannwischer @jakemas
We're building up a sizable array of highly complex proofs; cf. rejection sampling for example.
If a customer wants to understand what we are even proving by looking at the .ML themselves, they sometimes have to dig through >1000 LOC before finding the core theorems, and then they're not always marked as such or documented in detail.
We should consider introducing separate files for just the core theorems that we want the user to vet. It also makes review a bit easier, because we, too, should be content -- trusting the HOL-Light TCB -- to judge a proof contribution primarily based on its spec (primarily because there's also performance and maintainability concern, of course).
RFC @mkannwischer @jakemas