No need to forgive. You're not wrong nor naive. I'd pin the difference as one of personal risk tolerances. I have much less than you, that's all. Right now Solidity is the only choice of public smart contracts. All I meant before was that this is an impressive project and to be careful.
> But, after all, a dark horse 20 year old college dropout spearheaded the development of Ethereum, and the technology now secures nearly 20B worth of value.
This is a really common trope in finance -- the trader/quant/manager/pm who thinks that he's god's gift to earth because he made so much money (and a system that made even more). I'm not saying that's what's going on in Ethereum, far from it, just that people who make a lot of money tend to think they are worth that amount of money (usually they are just fortunate) and that using monetary value as the sole justification for one's actions is (generally) wrong.
While I disagree that Eth is actually valued at $20B -- if you can't get even a fraction of the $20B out of the market then it's not worth $20B in value... I bet the buy side of the Eth market supports around $100M-$300M max -- that's neither here nor there.
The Ethereum ecosystem is, invariant on the value it represents, truly impressive and Vitalik's work is amazing especially given his experience level prior to it. I wouldn't say that the EVM is well designed in the slightest but the rest of the system is. It's closer to a 80's era CPU than a modern VM. I get why it looks like it does -- taking the bitcoin bytecode and extending it as little as needed -- but I disagree with the approach at a technical level. VM's are supposed to do more (e.g. handle dispatch and library loading) and to not support that means one must implement it in the language (like an ASM compiler does) which in a blockchain context consumes the limited gas you have.
> I hold an optimistic view that, as formal verification techniques for smart contracts get fleshed out and easier to use
100% Agreed, though I don't think Solidity will have it anytime soon (3-5 year min for whole program verification that experts can use, I know some of the people working on it). The path the solidity FV people are following is a long, hard research path (close to what they did for the seL4 microkernel). Moreover, I know a ton about this because I built the first whole program formal verification system (compiler + DSL) for any smart contract language[1].
I built it for Pact, the language we[2] built to address the problems we saw with Ethereum's approach in enterprise contexts, that's FOSS but currently only available for on-chain use on our private platform. It wholly fixes the "immutable code" problem[3] via cryptocharters -- think of them as a module (smart contract) that have native support for both decentralized and centralized governance mechanisms for updating contracts and migrating the data they store. There's a bunch more stuff that Pact gets right, but that's what the papers are for describing.
Keep in mind that formal verification isn't the "end all be all" for program safety. While it massively advances the state of the art in that regard you need more than just FV because FV still requires human effort (just vastly less/safer than regular/auditing testing). It's just that FV is SO damn rare that most people, including myself until last year, (a) have no idea what it looks like and (b) have no idea what to use it for. People seem to think that an FV-capable language will solve all of their problems. No, it won't.
How many people going to become experts in SMT/Coq/Isabell just to write a safe smart contract? They, but Coq especially, make Haskell (which already scares people off) look like a cuddly puppy. What we'll need is a smart contract language that was designed to empower people to write safe code from the start + an FV system + a FV DSL that regular devs can use to leverage FV's power without having to become an expert in it. This is, unsurprisingly, exactly the feature set we have built for Pact. If you think I missed/should add a feature for empowering safe contracts I'm all ears (seriously, criticism/ideas are always welcome).
Wait a couple weeks and we'll have the public chain whitepaper(s) out (we're still refining the wording).
[1]: https://youtu.be/Nw1glriQYP8?t=1072 -- my co-founder is presenting it
[2]: http://kadena.io
[3]: "immutable code" gets you laughed out of the room in industry
Edit: this came out when I was writing the response... are you planning to sell tokens in the system? If so, again, be careful.
"SEC Issues Investigative Report Concluding DAO Tokens, a Digital Asset, Were Securities" https://www.sec.gov/news/press-release/2017-131