I had a look at this.
The overview is utterly incomprehensible to me. There are a lot of buzz words about things I know somewhere between little and nothing about. I am not competent to evaluate this, though the suspicion is raised that it is meaningless technobabble.
Then I clicked on one of the links, and
found this: The first part of this post makes sense to me, and accords more-or-less with my understanding of how Bitcoin and Etherium work, not that I know much about the latter. (Or the former, for that matter.) Then we get to this bit:
But it turns out that life aren't so easy. The Halting problem over Turing machines became so famous not because its answer is “No”, but because its answer is both “Yes” and “No”! A contradiction. This situation is mildly called “undecidability”. And this can go arbitrarily far: any such contradiction can be elevated to any statement, supplying a proof that it is true, and also supplying a proof that it is false!
Nonsense. The situation is called "undecidability" because there is no way to decide whether an arbitrary TM halts or not. The answer is not both "yes" and "no". It is one or the other, but we can't tell which. You should also understand that undecidability is not just a statement about our ignorance. It is built into the mathematics.
Undecidability is not a problem for the programmer. It's his job to ensure that
his program is decidable, and that it does what he wants it to do. Undecidability is (potentially) a problem for the people who run programs supplied by others. Etherium's solution to the halting problem - aborting the program when it runs out of "gas" - is the same as ours, and it is the correct solution. However the halting problem is not the only undecidable problem in computing and the issue will recur for us.
Because of such pathologies, we can never trust a proof over a Turing complete language. Completeness here happens to be precisely the completeness Godel spoke about, when he proved that any language that is expressive enough to describe arithmetic, must be either inconsistent or incomplete. Since Turing complete languages are also “Godel-complete”, they are provably inconsistent.
Utter balderdash. Turing-complete languages are languages which can compute anything a TM can. Godel-completeness means that any statement expressible in the language is also decidable in it. The very existence of undecidable problems shows that TMs are not Godel-complete.
At this point, you can stop reading. The author, who also appears to be the project leader, does not know what he's talking about.