If your willing to limit dynamic program behavior, then you get decidability pretty easily. As a really stupid, simple example, consider a programming language where you were allowed at most 5 lines of code, where each can perform operations on a single variable: incrementing or decrementing it. You’ll pretty easily be able to figure out if these programs terminate, all because you limited dynamic program behavior.

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.