How difficult is it to write correct smart contracts? Depends on your tools!
Formal method tools are key productivity aids for authoring correct smart contracts
In What properties must an enterprise smart contract language have?, Simon and Neil stated that “for a contract to be guaranteed to perform as intended, it must be amenable to formal verification methods.” In this blog post, we first discuss what formal methods are and why good language design greatly simplifies the task of applying formal methods. We then present the formal methods tools in use at Digital Asset for our contract modeling language, DAML. Readers with a strong background in formal methods may jump directly to the second part.