4 ms·

Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about an

Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about any weird runtime behavior and resource usage in a very rigorous way. Some of these things are still research problems and some of them are barely becoming practical in languages like Rust.

wyager 10y ago
> You want something that guarantees termination You usually get that through a restricted subset of an otherwise turing-complete language. The standard approach is to impose a finite metric on the arguments of a function and demonstrate that, as the function recurses, that metric monotonically approaches zero. >barely becoming practical in languages like Rust. As far as I know, this cannot be done in Rust. Agda, Coq, and Idris are the primary languages supporting termination checking (because they are syntactically suited for it). Haskell supports it as well through Liquid Haskell.
- dkarapetyan 10y ago
  I meant reasoning about resource usage. Rust provides lifetimes which I think is based on linear logic (see https://news.ycombinator.com/item?id=7061876 https://news.ycombinator.com/item?id=7061876). In theory, this gas thing should act as the metric you mentioned but it doesn't seem like it is implemented properly when it comes to how the fundamental building blocks of Solidity act with respect to the gas metric. The termination stuff in total languages I think has a ways to go in terms of general accessibility. Dependent types aren't the easiest thing to pick up.
  - wyager 10y ago
    Ah, that's an interesting idea. Static resource usage analysis instead of computation tokens. > Dependent types aren't the easiest thing to pick up. Look at liquid types. They're a lot easier to leverage in practice. Liquid Haskell is all just comments on top of a regular Haskell program.

wyager 10y ago

> You want something that guarantees termination You usually get that through a restricted subset of an otherwise turing-complete language. The standard approach is to impose a finite metric on the arguments of a function and demonstrate that, as the function recurses, that metric monotonically approaches zero. >barely becoming practical in languages like Rust. As far as I know, this cannot be done in Rust. Agda, Coq, and Idris are the primary languages supporting termination checking (because they are syntactically suited for it). Haskell supports it as well through Liquid Haskell.

dkarapetyan 10y ago
I meant reasoning about resource usage. Rust provides lifetimes which I think is based on linear logic (see https://news.ycombinator.com/item?id=7061876 https://news.ycombinator.com/item?id=7061876). In theory, this gas thing should act as the metric you mentioned but it doesn't seem like it is implemented properly when it comes to how the fundamental building blocks of Solidity act with respect to the gas metric. The termination stuff in total languages I think has a ways to go in terms of general accessibility. Dependent types aren't the easiest thing to pick up.
- wyager 10y ago
  Ah, that's an interesting idea. Static resource usage analysis instead of computation tokens. > Dependent types aren't the easiest thing to pick up. Look at liquid types. They're a lot easier to leverage in practice. Liquid Haskell is all just comments on top of a regular Haskell program.