Hacker News new | ask | show | jobs
by alphast0rm 3186 days ago
Isn't that something that can be helped by having a good standard library though (e.g. STL)? OpenZeppelin [1] is one example that comes to mind.

There are also other contract languages aimed to solve some of the limitations you mention, like Tezos/Michelson [2][3], which facilitate formal verification.

The issues you point out are certainly valid, but I believe people in the space are cognizant of them and are working on solutions.

[1] https://openzeppelin.org/

[2] https://www.tezos.com/

[3] https://www.tezos.com/static/papers/language.pdf
1 comments
pdkl95 3186 days ago
While a good standard library would help, the fundamental problem (undecidability) still exists. You could build a system that is understandable if you only use calls into a (presumably proven/tested to be safe) standard library. At that point it would de facto be a declarative language, which is decidable iff the grammar is not Turing complete[1].

It's limiting, but you can still have many of the fancier features by baking standard versions of them into the language/stdlib itself.

> I believe people in the space are cognizant of them and are working on solutions.

The problem with that is that this isn't a bug or engineering problem that we can solve with impossibly talented devs and a sufficiently large r&d budget. Questions about any non-trivial semantic behavior of a program (such as, "will the program halt"[2]) are known[3] too be undecidable[4].

[1] according to LangSec, the grammar needs to be deterministic context-free (or simpler). Anything more complex is undecidable.

[2] https://en.wikipedia.org/wiki/Halting_problem

[3] https://en.wikipedia.org/wiki/Rice%27s_theorem

[4] https://en.wikipedia.org/wiki/Undecidable_problem

link