As I understand it, Michelson (The language used to write smart-contracts in Tezos) is better suited for high-value applications where you want to extract strong correctness guarantees out of the code you write.
I think it's a promising development in the field (blockchain meets PLT)
You should check out Kadena's FOSS Pact[1] smart contract language as well.
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]
[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."
Michelson language is the smart contract language of Tezos, which is a competitor to Ethereum with flexibility in governance changes. Tezos is not fully live yet, but has active development.
Albert Michelson is one of the architects of the Michelson-Morley experiment, which was conceived to test for the existence of "aether" (ether). The experiments ultimately showed that ether does not exist.
"Ether" is also the name of the token that can be traded on the Ethereum blockchain, which some would consider a competitor of Tezos.
> Disclaimer: this contract can be attacked. Do not use the code in production unless you are aware of the risks you introduce.
I wish people didn't do this. If you're going to post an example, post correct/secure usage. People will copy and paste the code and it will end up in production.
Better to post no example at all than to post something you know is unsafe.
I don't see how this language enables writing safe contracts. You can still go wrong using the primitives (paraphrasing an example - "don't copy this contract I gave you to illustrate how to use my safer language because it can be attacked". The lower level primitives they discuss in the article would still make it hard to reason about what is happening. I think they need higher level operators that are trustworthy. You need a language that compiles down maybe into these primitives, but if you have operators that people reason about and trust you'll be more likely to be successful, like java synchronized.
I think it's a promising development in the field (blockchain meets PLT)
More resources on Michelson I found helpful:
https://youtu.be/4oG4Ead74xA
https://www.tezos.com/static/papers/language.pdf
https://www.reddit.com/r/tezos