4 ms·

No, you can't do an exhaustive search. Say you're a library author. You distribute pre-built library files. You've already lost because the compiler does not

No, you can't do an exhaustive search. Say you're a library author. You distribute pre-built library files. You've already lost because the compiler does not know your clients' code when it compiles your library. I am not kidding when I say it's provably impossible.

throwawaymaths 4y ago
"pre-built library files" are not a thing in zig right now, unless you use the c abi, which doesn't have async? Even supposing zig had prebuilding someday, you would probably have to extern it using async directly declared in the callconv (.async is an option in callconv) and so yes, the compiler would know. It's just that currently zig has a lot of "let the compiler figure out". Maybe that's what's making you uncomfortable? I'm pretty sure the zig compiler is finite and deterministic, so sophistry around the halting problem doesn't apply.
- gavinhoward 4y ago
  Wat. The Zig compiler is finite and deterministic, yes, but that's not the problem. The problem is that user code is not finite nor deterministic. Even worse, Zig's compiler may be deterministic and finite, but the language is not, by far. In fact, the language is one of the most infinite languages in existence because just the type system is uncomputable! [1] (In this context, the word "undecidable" used by that source means "uncomputable".) If the type system is uncomputable, then the type system will never be able to resolve all uses of function pointers everywhere. The whole point of the Halting Problem is that you could have a finite and deterministic Turing Machine that runs other Turing Machines, and that finite and deterministic Turing Machine could run into situation where it never halts. I never say this when people ask (because most people don't understand), but the real reason I don't like Zig is because of how infinite the language is, starting with its uncomputable type system. This makes Zig one of the most unreasonable [2] programming languages in existence. If you don't believe me, ask the Zig team how they plan to solve this problem. Don't ask them if they plan to solve it; ask them how. Then if they reply, email me [3] with their proposed solution, and I will destroy it. I will do that no matter how many solutions they come up with because math says I will always win. But if they say they can't, will you believe them? [1]: https://3fx.ch/typing-is-hard.html#zig https://3fx.ch/typing-is-hard.html#zig [2]: https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/ https://fsharpforfunandprofit.com/posts/is-your-language-unr... [3]: https://gavinhoward.com/contact/ https://gavinhoward.com/contact/
  - kristoff_it 4y ago
    > If you don't believe me, ask the Zig team how they plan to solve this problem. Don't ask them if they plan to solve it; ask them how. The Zig compiler has a counter that describes the maximum allowed amount of branching that the compiler can do while evaluating comptime code. The counter can be manually set to a higher value but all compilations will eventually fail if your comptime logic is too loopy. In practice the guideline is to not overuse comptime and instead create a dedicated build step for things like creating pre-computed value tables. > Then if they reply, email me [3] with their proposed solution, and I will destroy it. I will do that no matter how many solutions they come up with because math says I will always win. cringe
    - gavinhoward 4y ago
      > The Zig compiler has a counter that describes the maximum allowed amount of branching that the compiler can do while evaluating comptime code. Okay, here's a solution. It's already implemented. Nice. Now let me destroy it. You said those compilations "fail"; I presume there's an error that kicks in. In that case, then some valid Zig programs will be rejected, but your type system is now not technically Turing-complete. It's also less powerful; there are going to be things that Zig's type system cannot express. But wait; that's a user-defined setting? This means that either users will increase that setting when they need to and run into the same problem, or follow your guideline: > In practice the guideline is to not overuse comptime and instead create a dedicated build step for things like creating pre-computed value tables. It sounds like a dedicated build step would be the better option than comptime, to be honest. Also, if you step out to dedicated build steps, then the compiler no longer has complete visibility into that code when analyzing. At that point, the Halting Problem applies again. Also, what do you do if a user needs to pass a function pointer to a C function? I presume they must use a sync function? If so, that seems like a direct application of the function colors definition; some functions are unusable in certain places. If not, I'd be interested in what Zig does there.
      - kristoff_it 4y ago
        > In that case, then some valid Zig programs will be rejected, but your type system is now not technically Turing-complete. It's also less powerful; there are going to be things that Zig's type system cannot express. I think you're a bit too high on all this compsci theory stuff. All computations in all languages (including ones generally considered to be turing complete) fail when you run out of resources like RAM or patience. Zig introduces an artificial quantity that can be used as a machine-independent way to ensure all compilations eventually end in either success or failure. It's like a timeout, but an actual timeout would be inconsistent across different machines (with different performance characteristics). The actual state of things is much more boring than what your analysis tries to suggest: comptime is used to do some metaprogramming whose practical value is in good part determined by it not being too crazy, so the fact that you can't make a DisprovesCollatzConjecture type is actually fine. You have found another feature of Zig that's even more mundane than async where you're trying really hard to misunderstand everything to indulge in... "destroying". I think your own wording betrays the fact that you care about needlessly debating people more than actually understanding the tools in front of you in order to produce better software.

throwawaymaths 4y ago

"pre-built library files" are not a thing in zig right now, unless you use the c abi, which doesn't have async? Even supposing zig had prebuilding someday, you would probably have to extern it using async directly declared in the callconv (.async is an option in callconv) and so yes, the compiler would know. It's just that currently zig has a lot of "let the compiler figure out". Maybe that's what's making you uncomfortable? I'm pretty sure the zig compiler is finite and deterministic, so sophistry around the halting problem doesn't apply.

gavinhoward 4y ago
Wat. The Zig compiler is finite and deterministic, yes, but that's not the problem. The problem is that user code is not finite nor deterministic. Even worse, Zig's compiler may be deterministic and finite, but the language is not, by far. In fact, the language is one of the most infinite languages in existence because just the type system is uncomputable! [1] (In this context, the word "undecidable" used by that source means "uncomputable".) If the type system is uncomputable, then the type system will never be able to resolve all uses of function pointers everywhere. The whole point of the Halting Problem is that you could have a finite and deterministic Turing Machine that runs other Turing Machines, and that finite and deterministic Turing Machine could run into situation where it never halts. I never say this when people ask (because most people don't understand), but the real reason I don't like Zig is because of how infinite the language is, starting with its uncomputable type system. This makes Zig one of the most unreasonable [2] programming languages in existence. If you don't believe me, ask the Zig team how they plan to solve this problem. Don't ask them if they plan to solve it; ask them how. Then if they reply, email me [3] with their proposed solution, and I will destroy it. I will do that no matter how many solutions they come up with because math says I will always win. But if they say they can't, will you believe them? [1]: https://3fx.ch/typing-is-hard.html#zig https://3fx.ch/typing-is-hard.html#zig [2]: https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/ https://fsharpforfunandprofit.com/posts/is-your-language-unr... [3]: https://gavinhoward.com/contact/ https://gavinhoward.com/contact/
- kristoff_it 4y ago
  > If you don't believe me, ask the Zig team how they plan to solve this problem. Don't ask them if they plan to solve it; ask them how. The Zig compiler has a counter that describes the maximum allowed amount of branching that the compiler can do while evaluating comptime code. The counter can be manually set to a higher value but all compilations will eventually fail if your comptime logic is too loopy. In practice the guideline is to not overuse comptime and instead create a dedicated build step for things like creating pre-computed value tables. > Then if they reply, email me [3] with their proposed solution, and I will destroy it. I will do that no matter how many solutions they come up with because math says I will always win. cringe
  - gavinhoward 4y ago
    > The Zig compiler has a counter that describes the maximum allowed amount of branching that the compiler can do while evaluating comptime code. Okay, here's a solution. It's already implemented. Nice. Now let me destroy it. You said those compilations "fail"; I presume there's an error that kicks in. In that case, then some valid Zig programs will be rejected, but your type system is now not technically Turing-complete. It's also less powerful; there are going to be things that Zig's type system cannot express. But wait; that's a user-defined setting? This means that either users will increase that setting when they need to and run into the same problem, or follow your guideline: > In practice the guideline is to not overuse comptime and instead create a dedicated build step for things like creating pre-computed value tables. It sounds like a dedicated build step would be the better option than comptime, to be honest. Also, if you step out to dedicated build steps, then the compiler no longer has complete visibility into that code when analyzing. At that point, the Halting Problem applies again. Also, what do you do if a user needs to pass a function pointer to a C function? I presume they must use a sync function? If so, that seems like a direct application of the function colors definition; some functions are unusable in certain places. If not, I'd be interested in what Zig does there.
    - kristoff_it 4y ago
      > In that case, then some valid Zig programs will be rejected, but your type system is now not technically Turing-complete. It's also less powerful; there are going to be things that Zig's type system cannot express. I think you're a bit too high on all this compsci theory stuff. All computations in all languages (including ones generally considered to be turing complete) fail when you run out of resources like RAM or patience. Zig introduces an artificial quantity that can be used as a machine-independent way to ensure all compilations eventually end in either success or failure. It's like a timeout, but an actual timeout would be inconsistent across different machines (with different performance characteristics). The actual state of things is much more boring than what your analysis tries to suggest: comptime is used to do some metaprogramming whose practical value is in good part determined by it not being too crazy, so the fact that you can't make a DisprovesCollatzConjecture type is actually fine. You have found another feature of Zig that's even more mundane than async where you're trying really hard to misunderstand everything to indulge in... "destroying". I think your own wording betrays the fact that you care about needlessly debating people more than actually understanding the tools in front of you in order to produce better software.