> Decidability by limitation of dynamic program behavior
This claim sounds suspicious. If the authors really solved this, they have a bright future. A turing award for sure.
This claim sounds suspicious. If the authors really solved this, they have a bright future. A turing award for sure.
With this language, it looks like: they force all dynamically-sized objects (any string, any array) to set a maximum size at compile time, and limit loops to be statically sized (or on the length of one of those static sized objects). It feels like this gets them most of the way.
The missing bit is some reasoning about recursion: I didn’t look close enough to see what they do, but it seems like you could either disallow it (not great, but in the smart contracts I’ve written it’s not been super useful anyways), or you could do some sort of static reasoning about the recursive parameters to the function getting smaller (the gas accounting seems tricky here).
IMHO, the hard part of this language is convincing anyone the compiler is totally bug-free. In as hostile an environment as a blockchain, where a single bug can lead to all your money going bye bye, using a “new” language is a risk most people will choose to avoid, unless there is a seriously good reason to choose this new language.
IMO, decidability is not a killer-enough feature to convince people to take this risk.
https://github.com/clarity-lang/reference/blob/master/refere...
There's a game-theoretic argument that pretty much solves the issue: you pay money to run your smart contract.
The more it runs, the more it costs, until you run out of funds (gas).
Sounds pretty decidable to me.
But that would cost you such a large amount of money that no one does it.
In other words, the system, while breakable in theory, isn't in practice because of a set of economic incentives (or as it were, dis-incentives in this case).