lira VS hatlog

Lira[0] and its readable paper[1] is a good example of abstracting smart contracts into a statically typed, domain-specific language that describes the contract precisely at a high level. It's not Turing complete, which works for a large class of contracts (for instance, see the American and Asian options examples in [1]).

One concern with logic programming is cost of computation, on Ethereum every transaction has a gas associated with it and so you can't run computations that go over the gas available in a block.

Turner's ideas of Total Functional Programming[2] might have application in the smart contract space as well, since you disallow general recursion but allow structural recursion, you can likely precalculate or bound gas costs accurately ahead of time.

As for being statically typed, I completely agree, Solidity's poor design choices contributed to millions of USD in loss (e.g. DAO hack) because the developers were not able to easily reason about the implicit behavior or concurrency model.

[0] https://github.com/etoroxlabs/lira

[1] https://bahr.io/pubs/files/bahr15icfp-paper.pdf

[2] http://www.jucs.org/jucs_10_7/total_functional_programming/j...

A couple years ago I hacked on a Python type inferencer someone wrote in Prolog. I wasn't enlightened, despite expecting to be, from a bunch of HN posts like this.

https://github.com/andychu/hatlog

For example, can someone add good error messages to this? It didn't really seem practical. I'm sure I am missing something, but there also seemed to be a lot of deficiencies.

In fact I think I learned the opposite lesson. I have to dig up the HN post, but I think the point was "Prolog is NOT logic". It's not programming and it's not math.

(Someone said the same thing about Project Euler and so forth, and I really liked that criticism. https://lobste.rs/s/bqnhbo/book_review_elements_programming )