Programming Languages for Smart Contracts

I just read this paper (pdf related) about a "functional" language for smart contracts and it got me thinking... > How do you think languages for smart contracts should be designed? (Both from a practical and more theoretical perspective) > What do you think about the current state of the languages that are currently in use? To clarify: This thread is meant as a place to discuss language design for smart contracts. Please take discussion about practical smart contract development and debate about the viability, etc. of crypto currencies elsewhere.

In my opinion, smart contracts seem to be in the sweetspot for verified programs: They are not to unwieldy in scope because they don't do a lot of IO/data processing and they have high stakes (in the form of money) riding on them. I therefore think that smart contracts should be built in a way that allows for machine checked verification of them. I always thought that this would have to be embedded into the language, but the way Simplicity does it is actually pretty smart as well: The model the semantics of the language in Coq, which allows for proofs to be made there and makes the language building a lot simpler. That being said, Simplicity is way to weak of a language to be really practicable. I think a practical language should have totality checked recursion (a la Coq for example).

i sincerely hope this means that contract lawyers in the future will basically be programmers, because that's cyb as fuarrrk.