Home / Posts / Turing Complete Type Systems View Raw
18/06 — 2020
9.19 cm   0.9 min

Turing Complete Type Systems

Rust’s type system is Turing complete:

It is impossible to determine if a program written in a generally Turing complete system will ever stop. That is, it is impossible to write a program f that determines if a program g, where g is written in a Turing complete programming language, will ever halt. The Halting Problem is in fact, an undecidable problem.

How is any of this relevant?

Rust performs compile-time type inference. The type checker, in turn, compiles and infers types, I would describe it as a compiler inside a compiler. It is possible that rustc may never finish compiling your Rust program! I lied, rustc stops after a while, after hitting the recursion limit.

I understand that this post lacks content.

Hi.

I'm Akshay, programmer and pixel-artist.

I write open-source stuff to pass time. I also design fonts: scientifica, curie.

Send me a mail at [email protected] or a message at [email protected].

Home / Posts / Turing Complete Type Systems View Raw