Ghost of Departed proofs provides a fairly trivial way to generate proofs from arbitrary code and track them in the type system. See this article for example: h

Ghost of Departed proofs provides a fairly trivial way to generate proofs from arbitrary code and track them in the type system. See this article for example: https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized-these-ghosts.html https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized... This post shows a simple "positive" assertions, without any combinatorial logic associated with the proofs. But this is similar to programming by contracts.