Turing completeness vs decidable languages, safer smart contracts and running Ethereum on Ethereum.

Do we want Turing-completeness, or is a weaker model more suitable?

Would a dumber (not a Turing complete) language would make smart contracts smarter (easily verifiable)? We talk about total functional languages and alternatives to accounts-based model. Should we look at the blockchain as a pure data store, possibly equipped with primitives such as map/reduce or similar?

Links:

Meredith Pattersson talks about The Weird Machine https://archive.org/details/The_Science_of_Insecurity_

Tau Chain http://tauchain.org/

Idris: a general purpose pure functional programming language with dependent types http://www.idris-lang.org/

Safer smart contracts through type-driven development byt ROBERT EDSTRÖM, JACK PETTERSSON http://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf

Jack Pettersson and Robert Edström (Chalmers University of Technology, Sweden) present on a dependantly typed functional language for smart contracts. https://www.youtube.com/watch?v=H2uwUdzVD9I