Hacker News new | past | comments | ask | show | jobs | submit login

Um, no, that's just factually incorrect. You can do very, very many useful things without Turing completeness. You cannot be fully general, but there's active research on how far you can get. Restricted subsets of query languages like SQL and Datalog are perhaps the most common (though more or all SQL implementations are Turing complete) and indeed quite useful.

I can easily imagine a system built on a non-Turing complete logical query language that defines data and rules for presentation. You could get pretty far with that. You can't create _any_ application, but calling Turing completeness “essential … for decentralized applications” is incorrect. It's essential for a _subset_ of applications that require Turing completeness.

I've been saying ETH is broken for a while. Its computational ability means contracts _cannot_ be formally verified. This is why I didn't buy into the DAO, and sure enough there's a bug in the DAO (ironically recursion related).




People are under the impression that not being Turing complete is somehow enough to be feasibly verifiable. If we place (realizable) computational models on a scale, with 0 being no computation at all, and 10 being Turing completeness, then the computational models we can generally verify are somewhere between 0 and 1 (with 1 being, say, FSMs). A language with no loops, no recursion and just subroutines and binary variables -- i.e. it's an FSM -- is already PSPACE-complete to verify, meaning we can only verify only very short programs in that language. In other words, you need to get very far from Turing completeness to be generally verifiable.

This is why in general software verification doesn't try to come up with languages where all programs are verifiable, but aims to verify specific programs, sometimes regardless of the computational strength. Some programs in Turing complete languages can be verified (but certainly not all), just as some programs in FSM-strength languages can be verified (but certainly not all).

While it is certainly possible that a much bigger subset of, say, FSM programs can be verified than a subset of programs in TC languages, placing the bar at "Turing complete" is somewhat of a red herring.

Indeed, the LANGSEC link in the post[1] seems to understand that, noting that even verifying PDAs is undecidable, but it fails to note that even decidable verification tasks (for FSMs) are very often intractable, which -- for all practical purposes -- is just as bad as being undecidable.

[1]: http://langsec.org/occupy/




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: