If 'Sentinel' is Turing-complete, that's not a problem... right?


Well-known Member
Dec 22, 2015
With the disclaimer that I know nearly nothing about advanced math and nearly nothing about programming, I just wanted to post this thread I found which claims that Turing-complete languages don't allow anyone to know how they'll execute beforehand -- that you can only know what they'll do by executing them blindly.

The author is only making a case against Turing-complete languages in 'smart contracts.' I don't know if Sentinel qualifies as such, or if this is even relevant at all.

I just wanted to post this so that people more knowledgeable than I could verify one way or another.

Thanks. Here is the original link, and here is its opening:

(1) Turing-complete languages are fundamentally inappropriate for writing "smart contracts" - because such languages are inherently undecidable, which makes it impossible to know what a "smart contract" will do before running it.
(2) We should learn from Wall Street's existing DSLs (domain-specific languages) for financial products and smart contracts, based on declarative and functional languages such as Ocaml and Haskell - instead of doing what the Web 2.0 "brogrammers" behind Solidity did, and what Peter Todd is also apparently embarking upon: ie, ignoring the lessons that Wall Street has already learned, and "reinventing the wheel", using less-suitable languages such as C++ and JavaScript-like languages (Solidity), simply because they seem "easier" for the "masses" to use.
(3) We should also consider using specification languages (to say what a contract does) along with implementation languages (saying how it should do it) - because specifications are higher-level and easier for people to read than implementations which are lower-level meant for machines to run - and also because ecosystems of specification/implementation language pairs (such as Coq/Ocaml) support formal reasoning and verification tools which could be used to mathematically prove that a smart contract's implementation is "correct" (ie, it satisfies its specification) before even running it.

(continued here)​