HEADLINE: Pact is a human readable and Turing Incomplete smart contract language purpose-built for blockchains with powerful security features including full Formal Verification of user code, error messages, contract upgradability, support for interoperability, and strong permission and access control.