4 ms·

Yes (changed the post)... my point is that the program is valid! Rusts type system can fail to stop on valid programs. I’m probably making a mess of all this

• bodhiandphysics 6y ago
  Also I obviously fucked up the trivial proof. What I want to write is a rust program that type checks iff an an undecidable true proposition is true! But c doesn’t do that
• knome 6y ago
  type systems often feel like a rudimentary typeless haskell or prolog layered as a templating system over the underlying code, particularly if the types are used in generating code for generic types in the underlying typed language. for any reasonable program, you're not going to run into problems with the turing complete aspects of the type system. it's only when you start cleverly lifting logic into the type system to run in that typeless compile-time space that you'll feel punished by it. if you want to check if a type adheres to some constraint and then choose between different things to do, and then do that recursively et cetera, sure, you'll blow the template expansion stack. because you're not longer programming in the typed language, but in the typeless meta-language of its type system.