It’s embedded in a Turing complete language, but you can’t prove theorems about programs written in a Turing-complete language (Rice’s Theorem) so the ACL2 language itself has to be limited to programs that can be determined to halt. The J-Bob language from the book The Little Prover might be a better example.
Whether or not it's Turing-complete is not all that important. The important part is whether or not Turing-completeness is required for what is being created. In the case of HTML and CSS, Turing-completeness is almost always not a requirement.
Turing completeness is not a requirement for any computational task that is guaranteed to complete, either. You only need it to add infinite loop bugs.
Just to be clear - the things you actually care about expressing in a program don't require Turing completeness about 99.99999% of the time. The main exceptions are things like unbounded searches where the code will only terminate if it finds a solution to something, and there's no a priori size bound on the solution space.
We use Turing complete languages as a compromise. Proving your algorithm terminates to the satisfaction of a proof checker is often more work than it's worth. We've decided allowing bugs that a termination checker would prevent is less work to deal with than satisfying a termination checker. But for my daily work, Turing completeness is a practical compromise, not a necessity for expressing the algorithms I need to.
Comments
CSS + HTML is Turing complete:
https://lemire.me/blog/2011/03/08/breaking-news-htmlcss-is-t...
On the other hand, ACL2 isn’t Turing complete but can express many interesting programs: https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-man...
Are you sure ACL2 isn't Turing complete? I can't seem to find a proof of this.
It’s embedded in a Turing complete language, but you can’t prove theorems about programs written in a Turing-complete language (Rice’s Theorem) so the ACL2 language itself has to be limited to programs that can be determined to halt. The J-Bob language from the book The Little Prover might be a better example.
There’s a whole programming paradigm here of languages that aren’t Turing complete: https://en.m.wikipedia.org/wiki/Total_functional_programming
Whether or not it's Turing-complete is not all that important. The important part is whether or not Turing-completeness is required for what is being created. In the case of HTML and CSS, Turing-completeness is almost always not a requirement.
Turing completeness is not a requirement for any computational task that is guaranteed to complete, either. You only need it to add infinite loop bugs.
Just to be clear - the things you actually care about expressing in a program don't require Turing completeness about 99.99999% of the time. The main exceptions are things like unbounded searches where the code will only terminate if it finds a solution to something, and there's no a priori size bound on the solution space.
We use Turing complete languages as a compromise. Proving your algorithm terminates to the satisfaction of a proof checker is often more work than it's worth. We've decided allowing bugs that a termination checker would prevent is less work to deal with than satisfying a termination checker. But for my daily work, Turing completeness is a practical compromise, not a necessity for expressing the algorithms I need to.