The Michelson Language

Though it currently only runs on our (disclosure: am co-founder) high-performance private blockchain stack we're prepping it for use on a public blockchain (the first presale opens in Sept). It's a pretty different approach from Ethereum/Tezos in that it doesn't use a VM and instead is a Turing incomplete interpreted language (still metered though). You can think of it like LISP (for computational logic) + SQL (for storage) + Bitcoin script (for auth/capabilites logic).

Pact, like Tezos, supports direct whole-program formal verification but, unlike Tezos, you don't have to write in a stack-based language nor learn Coq/SMT to be able to use the FV system. It has a doc-string annotation DSL that describes the code's intended properties[2] so that non-PhD's can leverage at least some of formal verificaiton's power.

Also, like Tezos, Pact supports on-chain governance but, unlike Tezos, this governance doesn't perform a hard-fork and is instead limited to specific contracts and their data. As a touch of background, Pact has a native notion of modules, which syntactically require their upgrade workflow (i.e. governance), and imports. The upgrade workflow function's only requirement is that it is pass/fail (so it can be single-sig/multi-sig/decentralized vote/hybrid).

When a transaction attempts to perform an admin-only operation on a given contract the governance function fires which, if passed, grants the transaction admin-rights (allowing for arbitrary upgrades/data migrations/change governance) over the code and data the governance function protects. We expect voting-based governance to revolve around voting on the hash of a proposed transaction ahead of time (via other functions in the contract with interact with tables that record the vote) where the actual governance function's role is to tally the votes (fail if no winner) and then check that the triggering transaction's hash matches the hash that won.

Take the DAO debacle as an example: community leaders notice the problem and propose an upgrade which fixes the bug + refunds the affected users out the exploiter's account in the cold wallet + removes the exploiter's account -> users check that the upgrade does what it's supposed to and vote yay-nay on the upgrade -> community leaders submit the upgrade once it's won the vote. No hard forks, no white-hats, same result.[3]

[1]: http://kadena.io/try-pact

[2]: https://youtu.be/Nw1glriQYP8?t=1060

[3]: Given that the exploiter could attempt to shuffle their accounts once the upgrade is publicized, I'd expect this class of response to be closer to: spot the problem -> elect a board of directors to take control of the contract (users vote on this upgrade, effectively granting the board god-powers over the contract+data) -> board locks the contract -> board fixes the contract + refunds the impacted accounts -> board returns the contract to decentralized control.

PS: if you want a fun problem to chew on w.r.t. strong correctness consider this -- if smart contract B imports A (both are on-chain) and A later upgrades what should happen to B? B's author couldn't have tested/verified B's logic with A's new version as it doesn't exist yet so it shouldn't auto-upgrade (what if A has introduced an exploit intentionally?). Moreover, A may be upgrading to add new features (so previous versions of A maybe should still work) or it may be upgrading to fix an exploit (so previous versions should be banned).

In Pact we solve this problem by inlining the code used from A into B at creation. Thus, A's upgrade cannot change B's logic and B's author is assured that the code they tested/ran formal verification on is the only logic that will run until they decide to upgrade B. There is, however, one caveat: any inlined code from A that is impure (touches A's data/tables) is inlined with the version hash of A. Everytime B tries to execute A's code (even before A is upgraded) this hash it checked against a whitelist associated with A's data. If the hash isn't found, the transaction fails. When A upgrades, the authors can choose to grandfather in previous versions hashes of A (in the case of new features that don't conflict) or not (in the case of exploit upgrades). Thus, A can ban impure code but not pure code (equations).

We jokingly refer to it as the "no-leftpad approach."

I also found "Michelson: a Statically Typed Stack Based Language for Smart-Contract Execution - BPASE ’17" https://www.youtube.com/watch?v=4oG4Ead74xA