Oh awesome, glad you mentioned your project. I've actually been writing a blog post that parallels a lot of your complaints right here about Ethereum. For safety as well as implementation complexity, Turing completeness is a significant disadvantage for Ethereum, and I'm sorry to see it played up by so many as an advantage. Making a Turing-incomplete DSL need not be limiting and inexpressive, as you clearly know (and have shown).

I was thinking about creating a functional contract DSL that Coq could extract to. Not as familiar with Z3 and SMT solvers, but that's clearly another good approach to safety (I think Ethereum has finally started looking at formal verification after the DAO debacle, not sure what the status is. EDIT: looks like they've made a good bit of progress the past few months).

What about the status of your project? I see you've bootstrapped the contract language and a consensus protocol, do you plan on bootstrapping a P2P network? Or have you done that already and I missed it?