Knowing a bit of abstract algebra, semantics and type theory doesn't hurt. But I'd suggest to start by reading http://www.concrete-semantics.org/ http://www.con

Knowing a bit of abstract algebra, semantics and type theory doesn't hurt. But I'd suggest to start by reading http://www.concrete-semantics.org/ http://www.concrete-semantics.org/, which is a great overview. Once done, you can go for an approach well-grounded on the theories I mentioned above. I agree formal methods are great for smart contracts. Back in '08 when I was doing graduate work on the topic, some researchers were already talking about it, but the enabling technology (blockchain) was missing. They are also great for real-time critical systems, especially if you go with a formal methodology, where you start with some axioms (e.g. two trains can't be in the same track partition) and progressively derive your system from these by applying formally verified transformations till you end up with the code to deploy.