mercury VS hatlog

The Mercury compiler uses all of these techniques and more. Start here in the source code, and read the comments: https://github.com/Mercury-Language/mercury/blob/master/compiler/switch_gen.m

I'm not convinced there's great utility in smart contracts, but if there is, I think there's a huge utility in contracts being declarative and statically typed, to avoid many of the problems we've seen with existing contracts. In that case, a statically typed Prolog dialect would be a good starting point. The contract would be a set of declarative rules describing acceptable next states of the contract. To make the contracts verifiable in linear time, the submitter would submit the next state of the contract, plus a compact binary representation of the path taken through the rules set, so no backtracking would occur in the verifier. You could allow recursion, as verification time would still be linear in the size of the submitted compact path representation, just not linear in the size of the contract. If you disallow recursion, then verification would also be linear in the size of the contract.

Granted, many of the problems with Ethereum Solidity contracts are more to do with all of its use of implicit behavior (in a misguided attempt to hide the complexity of contracts) rather than directly consequences of Solidity being imperative.

Here's a quick plug for Mercury[0], a statically typed dialect of Prolog with an optimizing native code compiler. Supposedly it's 5 to 10 times faster than commercial Prolog compilers or available interpreters.

[0] https://github.com/Mercury-Language/mercury

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 )