This isn't necessarily a new idea. Tony Hoare discussed the idea for a while with his creation of Hoare triples; we are learning about the application right now in my Software Foundations course. It has a lot of interesting application within Coq for the analysis of the validity of programs, though. A good place to learn more about the application is here: https://softwarefoundations.cis.upenn.edu/current/plf-curren...