Hacker News Reader

Comment by cdumler | Hacker News Reader

This is the crux of the whole DeFi thing, and I strongly agree this was not a hack. My whole problem with DeFi is Gödel's Incompleteness Theorem. Roughly, it states that any reasonably complex code is going to have outcomes that cannot be determined by reading the code. In this case:

* Started with currencies that didn't allow flash loans. * Made a "we feel good about democracy of involvement" rule that supermajority could make any decisions with the funds "because we like people who invest in our work." * They added two currencies that supported flash loans. * Person or persons with currencies used flash loans to gain supermajority to transfer the funds out.

This is why banks are inefficient. There are (in theory) safeguards to transfers make it possible to stop or reverse activities. DeFi is forever going to be dealing with these issues after the fact.

View on HN

Applying the incompleteness theorem wouldn't say that every piece of complex code has unpredictable outcomes, but that there exists some pieces of code that have unpredictable outcome.

Seems like in this case the outcomes were entirely predicted by the "attacker".

Incompletness Theorem states that any system/language with primitive recursive arithmetic is either incomplete (since there is a construction of an undecidable statement via self reference) or unsound (since that same undecidable statement would be in contradiction)

AFAIK but speculating every programming language has primitive recursive arithmetic.

You are probably better off going with a computability theorem (such as the halting problem) instead of incompleteness. However, I suspect both will get you to the same place. Namely, there exists a program whose behavior cannot be predicted.

There is no theory that says that there does not exist a program whose behavior can be predicted. We have just criminally underfunded research into formal verification; and somehow decided that even computationally limited, code is law programs handling millions of dollars don't need any type of formal verification

What does a standard programming language being unsound even imply? It’s not being used for theorem proving, so how is it of consequence?

That it can produce contradictory results, if you have contradictions then at least one must be in error which means that following the language construction rules can produce erroneous results.

You could imagine a semantics that produces different results depending on the order of inference rules.

Yet another pseudoscientific application of Gödel’s incompleteness, which makes very specific guarantees about logical systems of a certain strength and their ability to prove theorems. I’ve no idea how you could twist it into what you suggest.

Reply on news.ycombinator.com