Oktahedron

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