It's possible to write provable programs in any language, but some formalisms make proofs easier than other. I think Michelson makes it easier. There are a few

It's possible to write provable programs in any language, but some formalisms make proofs easier than other. I think Michelson makes it easier. There are a few other advantages I can think of: 1) The code can be inspected directly on the blockchain and remain human readable. You can attach Solidity code to an Ethereum contract, but there is no certified compiler yet so you can't be sure they do the same thing. 2) Type safety and an insistence on functional design make good things happen. For instance, by insisting from the get go that contracts should be pure functions, we naturally make it hard to write DAO-like reentrancy bugs. By typing every input, we avoid the ABI bug that recently put some ERC20 funds at risk[1]. Good design principles help prevent problems before they occur. 3) The code can be made more concise. Adopting high-level primitives directly in the language, such as maps and lambdas, make it easier to do what you need with a small program. The language should reflect the type of problems encountered. For instance, building an "updatable" contract in Michelson can be done by putting the contract logic in a lambda and putting that lambda in the contract's storage. It can then be updated according to some logic, such as a multi-signature. Achieving the same thing in Ethereum is much more arduous. You could use a call to an external contract, and have the address of that contract updatable, but you lose all type safety and all isolation. [1] https://blog.golemproject.net/how-to-find-10m-by-just-reading-blockchain-6ae9d39fcd95 https://blog.golemproject.net/how-to-find-10m-by-just-readin...