@ltchen@mathstodon.xyz do you know what he's saying about "putting proof kernels inside abstract data types" in ML?