4 ms·

> Decidability by limitation of dynamic program behavior This claim sounds suspicious. If the authors really solved this, they have a bright future. A turing a

• crvdgc 5y ago
  I don't know if it's the case with this language, but in general it is possible to limit the expressiveness of a language to achieve decidability. The language cannot be Turing complete of course, but for example, we can have a language with the same computation power as finite automata, which is Turing decidable, and sometimes enough for the use case.
• narush 5y ago
  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.
  • nuclearnice1 5y ago
    Clarity also claims decidability. It gives up recursion and restricts looping. https://github.com/clarity-lang/reference/blob/master/reference.md https://github.com/clarity-lang/reference/blob/master/refere...
  • preseinger 5y ago
    You are trying to re-discover Turing completeness from first principles and apparently without the relevant theoretical background.
• ur-whale 5y ago
  Not sure decidability is that much of an issue for smart contract language. 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.
  • whimsicalism 5y ago
    I agree but have no idea how that relates to game theory.
    • ur-whale 5y ago
      In theory it's possible to let your dapp run forever, hogging resources from the network and "breaking" the system. 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).
• mgraczyk 5y ago
  All EVM programs that run on Ethereum are trivially decidable because of the per-block gas limit ;P