3 ms·
This seems wrong. If you require a proof that a program halts for all input (or of any halting equivalent property), then there will be programs you cannot wri
by dllthomas 5y ago
This seems wrong. If you require a proof that a program halts for all input (or of any halting equivalent property), then there will be programs you cannot write - those that possess the property in question but for which no proof exists, and those that actually lack the property.
In particular, you obviously cannot write a universal Turing machine in a system that requires a proof of halting for all input, because it by definition won't halt if it is fed a program that does not halt. A system that cannot build a UTM is not Turing complete.
- naasking 5y agoI'm not sure what exactly is not right. Type-based theorem provers exist (Coq, Idris, Agda, etc.). They can be used to write Turing complete programs (eg. CompCert). If you encode the properties that need to be satisfied and the compiler successfully compiles your program, then those properties are satisfied. I suspect you've simply misunderstood the claims that were made. In particular, the above does not entail that you can write any program. Some programs simply have no valid type.
- dllthomas 5y agoI guess that I am claiming that using Coq, Idris, Agda, etc, (in a setting where we are actually using them to prove correctness properties that are halting equivalent), is itself a particular way of working in a language that is not Turing Complete. As an aside, "Turing complete programs" seems like a category error?