Comment by ianhorn

Not the author, but I've been doing this kind of thing with Lean. I'm still trying to figure out how to make this workflow play nicely with other systems. I have a bunch of rust code that I want these kinds of guarantees on, and that code has third party dependencies that would be terrible to give up. It's totally unclear right now how to get the best of both worlds.