5 ms·

The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine

by mbrock 9y ago

The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language. Turing completeness makes it hard to prove properties automatically about arbitrary programs, but you can still prove properties about specific programs. I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc.

seanwilson 9y ago
> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with expensive computations have bad impacts on the network? Their "gas" system is their way of dealing with that and perhaps you would still need something similar even with a total language. I can't think of program verification research where both termination and CPU cost is verified. I can think of some papers that deal with identifying Big Oh growth rates though. Either way, smart contracts sound like one of the top tier areas where you want strong static typing that has a route to be formally verified.
- grogenaut 9y ago
  I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
  - seanwilson 9y ago
    What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
    - grogenaut 9y ago
      Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
      - seanwilson 9y ago
        I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact. General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
        grogenaut 9y ago
        I guess that makes sense to count axioms as strongly typed.
    - tom_mellior 9y ago
      (Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.
  - Cybiote 9y ago
    Dependent or even refinement type systems are where a great deal of research into proof carrying code is done (for refinement types, since systems are restricted to decidability, the proofs are automatic but more limited).
  - UncleMeat 9y ago
    Type checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.
- mbrock 9y ago
  The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period.
  - seanwilson 9y ago
    > The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period. Exactly, knowing that the contract code will eventually halt is nice to know but knowing that it will halt after a reasonable CPU cost seems much more important in this case (which is really interesting). From what I've seen from example contracts, it doesn't seem like the chance of infinite loops is that high. Personally, I find that in mainstream languages, if you accidentally write an infinite loop you find out very quickly on the first few runs and code that could be hiding an infinite loop stands out. The vast majority of loops just iterate from the start of a collection to the end.
    - mbrock 9y ago
      The contract coders I work with try as much as possible to avoid loops altogether, because even if they're correct, they'll still have a linear cost, and that's usually not what you want. Almost all contract operations should be O(1). Sometimes we've made fairly large system design changes to avoid a loop in a function.
      - seanwilson 9y ago
        Interesting. So what's your view about the most practical language for writing contracts in then? For what I've read, having the sender setting gas limits seems really awkward especially when the limit is exceeded. Are there practical alternatives? Even with O(1) you'd need to limit the computation time.

by mbrock 9y ago

seanwilson 9y ago

> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with expensive computations have bad impacts on the network? Their "gas" system is their way of dealing with that and perhaps you would still need something similar even with a total language. I can't think of program verification research where both termination and CPU cost is verified. I can think of some papers that deal with identifying Big Oh growth rates though. Either way, smart contracts sound like one of the top tier areas where you want strong static typing that has a route to be formally verified.

grogenaut 9y ago
I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
- seanwilson 9y ago
  What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
  - grogenaut 9y ago
    Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
    - seanwilson 9y ago
      I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact. General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
      - grogenaut 9y ago
        I guess that makes sense to count axioms as strongly typed.
  - tom_mellior 9y ago
    (Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.
- Cybiote 9y ago
  Dependent or even refinement type systems are where a great deal of research into proof carrying code is done (for refinement types, since systems are restricted to decidability, the proofs are automatic but more limited).
- UncleMeat 9y ago
  Type checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.
mbrock 9y ago
The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period.
- seanwilson 9y ago
  > The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period. Exactly, knowing that the contract code will eventually halt is nice to know but knowing that it will halt after a reasonable CPU cost seems much more important in this case (which is really interesting). From what I've seen from example contracts, it doesn't seem like the chance of infinite loops is that high. Personally, I find that in mainstream languages, if you accidentally write an infinite loop you find out very quickly on the first few runs and code that could be hiding an infinite loop stands out. The vast majority of loops just iterate from the start of a collection to the end.
  - mbrock 9y ago
    The contract coders I work with try as much as possible to avoid loops altogether, because even if they're correct, they'll still have a linear cost, and that's usually not what you want. Almost all contract operations should be O(1). Sometimes we've made fairly large system design changes to avoid a loop in a function.
    - seanwilson 9y ago
      Interesting. So what's your view about the most practical language for writing contracts in then? For what I've read, having the sender setting gas limits seems really awkward especially when the limit is exceeded. Are there practical alternatives? Even with O(1) you'd need to limit the computation time.