You might be interested in the YNot[1] project, which is a library implementing Hoare-style axiomatic semantics in Coq. Just using Coq as the proof language ans

You might be interested in the YNot[1] project, which is a library implementing Hoare-style axiomatic semantics in Coq. Just using Coq as the proof language answers a lot of your questions since Coq has well-understood limitations designed to make it useful for automatic proofs. If you're not familiar with the idea of dependent types, it's definitely worth learning about them (and Coq is a good place to start) because they formalize the idea of arbitrary functions at the type level by letting types depend on values, giving you the ability to verify whatever invariants you like. A good place to start would be Benjamin Pierce's free Software Foundations[2] book. There's a really rich theory here with a lot of both theoretical and practical problems worked out but, at the same time, lots of room to develop new ideas and approaches if this is something you're interested in. [1]: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ [2]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html