Those are currently not the issues that require attention.
You can make it as fast and as large as you want, if it is broken at the root that's all pointless. First walk, then run. I'd be more impressed with a much smaller system without sharding and massive scaling properties if it was bullet proof.
Ethereum itself is more bullet proof, as there are multiple implementations and the description of the protocol better defined and has proofs inside.
That's the whole problem in a nutshell. I highly doubt that is the road to a viable solution but I'm patient enough to be proven wrong in the longer term. But anything that is Turing complete automatically implies that anything layered on top of it will incorporate such niceties as being impossible to formally verify due to the halting problem.
In other words: the only way to establish whether or not the code will try anything funny is to run it.
Whenever you want any guarantees about anything you implement a very restricted[1] subset of what a TM can do... at least if you're allowing users to input arbirtrary programs[2]. If you don't restrict to a non-TC language... you're -- in so many words -- fucked. (Hence the "hack".)
[1] Preferably using a statically typed PL, for obvious reasons. There's actually a thing these days where non-TC languages can actually "do things". My favorite moniker for this is "pacman-complete" (coined by Edwin Brady, I believe.)
[2] Having looked at a few .sol files earlier, they at least look TC, having general recursion and all.
Not sure I follow here... You can certainly run a non-turing-complete language on top of a turing-complete one and anything in that language could potentially be verifiable.
Edit: apparently the thefts so far are "only" 45 million.
Just kidding; bad joke; I just couldn't resist.
This is what happens when one does not do that. :)