How bound are people to using Solidity? How hard would it be to come up with a competing, more verifiable langauge specification? I don't know much about Ethereum, but I assume the Solidity gets compiled to some sort of bytecode to run on the VM?
Not at all. Solidity is just the most widely used language for the EVM. There are also Mutan (dead), Serpent (dying), LLL (recently revived), and Viper (being drafted).
