12 ms·

I've a similar question to GP, but from a slightly different angle. I can see the attraction of using a Turing complete language, but on the other hand, an impo

I've a similar question to GP, but from a slightly different angle. I can see the attraction of using a Turing complete language, but on the other hand, an important properly of a build system is that it ought to halt at some point. Something like, say, Starlark, which is used in Bazel, is primitive recursive, so it's not Turing complete, but gets you almost all the way to Turing complete while also being guaranteed to halt. It'd be interesting to see this aspect covered. EDIT: s/Skylark/Starlark/

gavinhoward 3y ago
I'm afraid I have bad news. The thing about Starlark is that it is effectively Turing complete. You can simulate a while loop with a long enough foreach, an if statement, and a break statement. And by "long enough," I mean long enough to make anyone just stop the build, but hey, if I stack the foreach loops, I can make the inner loop exponentially long, even though ints are limited to 32 bits. By not taking out the break keyword, Starlark remains Turing-complete. And yes, I tested this.
- talideon 3y ago
  That's not Turing complete. That's still primitive recursive. You're going out of your way make it loop for a really, really long time, but it's still guaranteed to terminate, and thus isn't Turing complete, even if it'd take a really long time to terminate. This isn't some theoretical thing: it's how you can introduce guarantees into the system that it can't get out of control by accident and it also makes it easier to reason about the system. A primitive recursive language gets you most of the benefits of a general recursive one _without_ needing to be _actually_ Turing complete. So this isn't "bad news" for me. I'm saying that I think you should avoid using a general recursive (i.e. Turing complete) language for a build system and instead have guarantees that the system will terminate by using a primitive recursive language of some kind because you literally, as you did, need to go out of your way to get code written in such a fashion to run for an inordinate amount of time. And yet, an inordinate amount of time isn't forever and unlike a program written in an actually Turing complete language, you can use static analysis to detect that kind of thing if only primitive recursion is supported.
  - gavinhoward 3y ago
    > And yet, an inordinate amount of time isn't forever If it's only guaranteed to terminate after the heat death of the universe, it won't terminate, so I would call that "forever." > unlike a program written in an actually Turing complete language, you can use static analysis to detect that kind of thing if only primitive recursion is supported. And this is exactly why I said that break was necessary. Sure your static analysis may detect that the loop goes 2^256 times, which would be "forever," and so it returns the answer, "Does not halt." Ah, but with the break keyword, it still could. In fact, it might always halt rather quickly. Rule of thumb is that if static analysis can be wrong, it is Turing-complete.

gavinhoward 3y ago

I'm afraid I have bad news. The thing about Starlark is that it is effectively Turing complete. You can simulate a while loop with a long enough foreach, an if statement, and a break statement. And by "long enough," I mean long enough to make anyone just stop the build, but hey, if I stack the foreach loops, I can make the inner loop exponentially long, even though ints are limited to 32 bits. By not taking out the break keyword, Starlark remains Turing-complete. And yes, I tested this.

talideon 3y ago
That's not Turing complete. That's still primitive recursive. You're going out of your way make it loop for a really, really long time, but it's still guaranteed to terminate, and thus isn't Turing complete, even if it'd take a really long time to terminate. This isn't some theoretical thing: it's how you can introduce guarantees into the system that it can't get out of control by accident and it also makes it easier to reason about the system. A primitive recursive language gets you most of the benefits of a general recursive one _without_ needing to be _actually_ Turing complete. So this isn't "bad news" for me. I'm saying that I think you should avoid using a general recursive (i.e. Turing complete) language for a build system and instead have guarantees that the system will terminate by using a primitive recursive language of some kind because you literally, as you did, need to go out of your way to get code written in such a fashion to run for an inordinate amount of time. And yet, an inordinate amount of time isn't forever and unlike a program written in an actually Turing complete language, you can use static analysis to detect that kind of thing if only primitive recursion is supported.
- gavinhoward 3y ago
  > And yet, an inordinate amount of time isn't forever If it's only guaranteed to terminate after the heat death of the universe, it won't terminate, so I would call that "forever." > unlike a program written in an actually Turing complete language, you can use static analysis to detect that kind of thing if only primitive recursion is supported. And this is exactly why I said that break was necessary. Sure your static analysis may detect that the loop goes 2^256 times, which would be "forever," and so it returns the answer, "Does not halt." Ah, but with the break keyword, it still could. In fact, it might always halt rather quickly. Rule of thumb is that if static analysis can be wrong, it is Turing-complete.