I don't have a fully formed view yet, but I think Solidity is a pretty good prototyping language, disregarding all marketing hype that it's an "easy" language. While developing, you'd also be working on a specification of exactly how the contract shall behahve, and trying very hard to simplify ruthlessly.

The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Right now I'm working on tools for static analysis of bytecode and using such tools to verify the correctness of contracts written by hand in assembly, which I think makes a great deal of sense for the simple contracts that we need as utilities (multisigs, tokens, etc).

> The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Yeah...any ideas why they didn't go with a language that had an easier route for formal verification? It seems like an ideal application and the contract specifications seem like they would be fairly straightforward to prove (compared to what you'd see in most journal papers for instance). I'm guessing the designers just weren't aware of theorem provers but I'm puzzled why they didn't go with a language with strong static typing where private access and immutability are the defaults plus avoiding anything to do with the mechanism they have for picking default handling functions when a message isn't understood. Great experiment to watch though!