Embedding functional smart contract languages into the Coq proof assistant

[ataraxiaceleste]

Bas Spitters and Danil Annenkov of Concordium have proposed a novel way of embedding functional smart contract languages into the Coq proof assistant using meta-programming techniques.

Their framework allows for developing the meta-theory of smart contract languages using the deep embedding and provides a convenient way for reasoning about concrete contracts using the shallow embedding. They mainly propose an approach that allows to make a connection between the two embeddings in a form of a soundness theorem.

As an instance of their approach they develop an embedding of the Oak smart contract language in Coq and verify several important properties of a crowdfunding contract.

They claim that they have developed techniques that are applicable to all functional smart contract languages thorough this.

I know that this can be a technically heavy subject.But wondering if any researchers or any other blockchain projects have gone down this route?

[LiamJohn]

Together, the smart contract and the Coq proof assistant have the potential to change almost every area of our society. But we need to wait to see if these disruptive technologies can overcome many hurdles to be adopted on a large scale.