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?
Pact is live and in-use in enterprise settings on our permissioned blockchain platform; you can download the interpreter which when launched with "-serve" presents the RPC REST API, allowing you to write whole applications with just the interpreter; indeed there's a sample "TODO MVC" app showing just how easy this is (see https://github.com/kadena-io/pact/blob/master/README.md).
As for a public platform, stay tuned, we will have an annoucement very soon. Suffice to say for now: any work you do using Pact will have a public chain to run on in the very near future; you can use the O/S releases to develop Pact; and if you have an idea about permissioned (think "B2B only") blockchain applications, get in touch!
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?