[qwtel]

I've been wondering if non-turning complete languages might be the way to go for many smart contracts, which often resemble vending machines more than what general purpose languages are used for. Those should be captured by pushdown automaton or even a finate state machine and the corresponding languages (but except from regex, I'm not really aware of any..).

My CS knowledge got really rusty, but I think it should be possible to put tight bounds on the computational cost of these, as well as statically guarantee that certain states cannot be reached, both of which would be very valuable in this case.