Interactive theorem provers can quickly get you from stage 1 to 2.
If you are interested, [1] describes the experience of a professor teaching how to write correct and readable proofs about program semantics using the interactive theorem prover Isabelle/HOL.
Isabelle/HOL can make you learn fast because it allows one to get instant feedback on a proof. Proving things may then become surprisingly addictive.
If you are interested, [1] describes the experience of a professor teaching how to write correct and readable proofs about program semantics using the interactive theorem prover Isabelle/HOL.
Isabelle/HOL can make you learn fast because it allows one to get instant feedback on a proof. Proving things may then become surprisingly addictive.
[1] http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf