Hacker News Reader

Comment by johnbender | Hacker News Reader

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.

View on HN

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.

> 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.

I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq.

UPDATE: found it thank you.

Stupid question, isn't this the Halting Problem?

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.

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".

The important word there was “every”.

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).

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.

> 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.

I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.

Which is why the language is not Turing complete

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/...

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-...

[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/5b546b9039a8cf8f28e0b8...

Reply on news.ycombinator.com