Personally, I've always wanted take a look at Liquidity Lang [0] which exists on top of Michelson. At a glance, it seems to solve a large number of issues that have caused bugs in Solidity smart contracts (e.g. liquidity has abstract data types, disallows inline mutation of state, etc)
[0] http://www.liquidity-lang.org/