top | item 40061576

A proof that Meson is Turing-Complete

11 points| d_tr | 1 year ago |github.com | reply

10 comments

order
[+] tromp|1 year ago|reply
> Mathematically speaking, no modern lanaguage is turning-complete because memory size on any machine has a fixed upper-bound.

Many languages have no memory limit. Some do not even have a notion of memory (e.g. lambda calculus). Language implementations on physical machines do suffer from memory limits though.

Meson only allows bounded loops, so technically it's not Turing complete. But the author claims:

> ## Loop over 2^64 elements, this is effectively an infinite loop

[+] WCSTombs|1 year ago|reply
Yeah. It seems by the author is effectively arguing that general recursion and primitive recursion are equivalent. There seems to be a pretty fundamental failure of logic here.
[+] pron|1 year ago|reply
Turing completeness is a red herring in such contexts. People who may know about the undecidability of halting for programs in Turing complete languages are under the impression that if a language is not Turing complete (and is therefore decidable), then analysing a program in such a language would generally be easier in practice (if not downright easy) than a program in a Turing complete language. This is quite simply completely and utterly wrong, because decidability is not a relevant bar for feasibility (tractability). TQBF [1] is already well beyond our practical powers of sound program analysis (and there aren't even good heuristics as for SAT), and to be reducible from TQBF all you need are boolean variables and either functions (even if recursion is disallowed) or loops restricted to two iterations (corresponding to quantifying over true and false). Even P=NP won't help you when you're PSAPCE-complete.

In other words, once you're PSPACE-complete, sound analysis is already intractable. Not being Turing complete makes no further practical difference ("sure, analysing a program will take longer than the heat-death of the universe, but we take comfort in the fact that it's bounded!"). Decidability is an older and more famous notion than tractability, but in computational complexity and in program analysis we care about the latter (the former matters only so far as if something is undecidable then it's also intractable).

[1]: https://en.wikipedia.org/wiki/True_quantified_Boolean_formul...

[+] humanrebar|1 year ago|reply
> I don't think this proof invalidates any of the excellent work that has been put into Meson. If anything, this shows that build configuration is a hard enough problem that requires a turing-complete language. Most features have gone into Meson because somebody actually needed them. And for this reason, Meson serves as an estimate of the required complexity.

I think it's true given the goal to support a specific set of requirements of modern build systems.

The problem is that there is no separate dependency management protocol to target, and there is no separate projects description configuration format. That means build systems end up trying to interoperate with, or even implement large portions of, those kinds of subsystems.

[+] kitd|1 year ago|reply
Very cool. Now do a Lisp!

BTW, Meson is the simplest C/C++ build system I know yet, great for small and/or personal projects.

[+] mark_undoio|1 year ago|reply
We converted our product (which I'd say is medium-sized - it's not a sprawling enterprise codebase but it's the work of a team over many years) to use Meson for its C / C++ components and I've been very pleased with it.

It's pretty straightforward to understand, has good documentation and it's fast.