3 ms·

A few thoughts/questions if the authors stop by since I can't seem to find a link to the Coq source: I'm curious if there is an interpreter written in Gallina

A few thoughts/questions if the authors stop by since I can't seem to find a link to the Coq source: I'm curious if there is an interpreter written in Gallina that implements the semantics? Maybe with a simulation proof (or similar)? It would be pretty sweet to have a verified interpreter. Also, found this in the corresponding blog post while search for the Coq source. > It is Turing incomplete, disallowing unbounded loops and allowing for static analysis It's definitely possible (and not so hard depending) to do proofs and static analysis of looping programs provided the specification can be encoded as an invariant. To be fair I'm not sure what the implications of non-terminating programs are in this setting and with respect to a specification.

jmgrosen 9y ago
> I'm curious if there is an interpreter written in Gallina that implements the semantics? Assuming you only want the core language, the semantics is an interpreter -- available in Appendix A.
- johnbender 9y ago
  I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq. UPDATE: found it thank you.
netsec_burn 9y ago
Stupid question, isn't this the Halting Problem?
- johnbender 9y ago
  Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
  - schoen 9y ago
    I keep encountering what I think is a misunderstanding of Rice's Theorem. Rice's Theorem says no program can correctly decide any nontrivial property for every program. However, there are programs that can correctly decide nontrivial properties for many programs! To avoid the Rice's Theorem issue, you just need to be able to say "Don't know"/"Couldn't decide".
    - kobeya 9y ago
      The important word there was “every”.
      - schoen 9y ago
        Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
        nullc 9y ago
        This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner. An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction. It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case. In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
- hossbeast 9y ago
  Which is why the language is not Turing complete
- mietek 9y ago
  This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit uncontrolled general recursion. (Likewise for Rice's theorem.) Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps. See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/master/doc/pdf/turner-2004.pdf https://github.com/mietek/total-functional-programming/blob/... Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving. Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...
kobeya 9y ago
The paper seems to address this. It notes that some loop constructs could be made available but it would make the resource consumption estimation unnecessarily conservative. Note that you can do things like unroll a loop entirely and build a Merkle tree of the possible unrolled versions, just revealing at redemption time the one actually used.

jmgrosen 9y ago

> I'm curious if there is an interpreter written in Gallina that implements the semantics? Assuming you only want the core language, the semantics is an interpreter -- available in Appendix A.

johnbender 9y ago
I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq. UPDATE: found it thank you.

netsec_burn 9y ago

Stupid question, isn't this the Halting Problem?

johnbender 9y ago
Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
- schoen 9y ago
  I keep encountering what I think is a misunderstanding of Rice's Theorem. Rice's Theorem says no program can correctly decide any nontrivial property for every program. However, there are programs that can correctly decide nontrivial properties for many programs! To avoid the Rice's Theorem issue, you just need to be able to say "Don't know"/"Couldn't decide".
  - kobeya 9y ago
    The important word there was “every”.
    - schoen 9y ago
      Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
      - nullc 9y ago
        This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner. An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction. It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case. In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
hossbeast 9y ago
Which is why the language is not Turing complete
mietek 9y ago
This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit uncontrolled general recursion. (Likewise for Rice's theorem.) Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps. See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/master/doc/pdf/turner-2004.pdf https://github.com/mietek/total-functional-programming/blob/... Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving. Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...

kobeya 9y ago

The paper seems to address this. It notes that some loop constructs could be made available but it would make the resource consumption estimation unnecessarily conservative. Note that you can do things like unroll a loop entirely and build a Merkle tree of the possible unrolled versions, just revealing at redemption time the one actually used.