5 ms·

> Isn't compiling several languages, including Rust, actually undecidable though? While Rust is Turing complete, the compiler has a recursion limit, and if you

> Isn't compiling several languages, including Rust, actually undecidable though? While Rust is Turing complete, the compiler has a recursion limit, and if you take that into account, then compiling Rust is decidable (you only need to evaluate compilation up to the recursion limit).

ghosty141 5y ago
Rusts type system is turing complete if I recall correctly. Obviously, in practice everything is in a way decidable because we have limitations everywhere.
- lovasoa 5y ago
  There is a low hardcoded limit to how deep you can nest types. But I don't think there is a hardcoded limitation to how large match patterns can be. That's the difference.
  - smitop 5y ago
    It's possible to change that hardcoded limit. By default it is 256, but you can bring it all the way up to 2^64 with #![recursion_limit = "18446744073709551615"].
- derefr 5y ago
  In other words, the abstract machine specification you’re programming your compile-time logic against in Rust, has Turing-complete semantics; but its extant implementations — any Rust compiler people would care to use — intentionally does not implement compile-time Turing-completeness. But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete; and that compile-time runtime would be conformant to the Rust language spec. (Just, nobody would want to use it, because “unbounded runtime” isn’t a property people tend to want from their compilers.)
  - dllthomas 5y ago
    > But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete Only if your theory allows for infinite storage...
    - einpoklum 5y ago
      Well, my infinite tape seemed to work just fine last time I checked. Of course, I didn't check ad infinitum. <rim shot>
  - volta83 5y ago
    There is nothing preventing the Rust language definition to add a constraint to type checking saying "recursion depth <= 128" or something like that (e.g. depth <= N where N is an implementation-defined constant). In fact, since rustc is "the spec" today, that's kind of how it is ""specified"". Any implementation that does not conform to that would be... non-conforming... or using your own point-of-view, they would be implementing some programming language, but that language wouldn't be "Rust". Then the question is not if Rust programs type-check in finite time, but rather, whether they type check in <= N steps. And e.g. the current implementation answers that question very quickly by just trying.
pjmlp 5y ago
Same applies to C++ templates by the way, the compilers usually provide an expansion depth flag.

ghosty141 5y ago

Rusts type system is turing complete if I recall correctly. Obviously, in practice everything is in a way decidable because we have limitations everywhere.

lovasoa 5y ago
There is a low hardcoded limit to how deep you can nest types. But I don't think there is a hardcoded limitation to how large match patterns can be. That's the difference.
- smitop 5y ago
  It's possible to change that hardcoded limit. By default it is 256, but you can bring it all the way up to 2^64 with #![recursion_limit = "18446744073709551615"].
derefr 5y ago
In other words, the abstract machine specification you’re programming your compile-time logic against in Rust, has Turing-complete semantics; but its extant implementations — any Rust compiler people would care to use — intentionally does not implement compile-time Turing-completeness. But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete; and that compile-time runtime would be conformant to the Rust language spec. (Just, nobody would want to use it, because “unbounded runtime” isn’t a property people tend to want from their compilers.)
- dllthomas 5y ago
  > But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete Only if your theory allows for infinite storage...
  - einpoklum 5y ago
    Well, my infinite tape seemed to work just fine last time I checked. Of course, I didn't check ad infinitum. <rim shot>
- volta83 5y ago
  There is nothing preventing the Rust language definition to add a constraint to type checking saying "recursion depth <= 128" or something like that (e.g. depth <= N where N is an implementation-defined constant). In fact, since rustc is "the spec" today, that's kind of how it is ""specified"". Any implementation that does not conform to that would be... non-conforming... or using your own point-of-view, they would be implementing some programming language, but that language wouldn't be "Rust". Then the question is not if Rust programs type-check in finite time, but rather, whether they type check in <= N steps. And e.g. the current implementation answers that question very quickly by just trying.

pjmlp 5y ago

Same applies to C++ templates by the way, the compilers usually provide an expansion depth flag.