3 ms·
> To the right, in this context, means more statically typed. While the notion is natural, the sentence is uninformed. When I wrote the article, I hadn't yet r
by darawk 5y ago
>
To the right, in this context, means more statically typed. While the notion is natural, the sentence is uninformed. When I wrote the article, I hadn't yet read Charles Petzold's excellent Annotated Turing. Although I had heard about the halting problem before reading the book, I hadn't internalised it. I wasn't able to draw inferences based on that labelled concept.
> After I read the book, I've come to understand that general-purpose static type system can never prove unequivocally that a generic program works. That's what Church, Turing, and Gödel proved.
This is not exactly the right inference. You can have a language that has the property "if it compiles, it works", that language just cannot also be Turing complete.
- naasking 5y ago> This is not exactly the right inference. You can have a language that has the property "if it compiles, it works", that language just cannot also be Turing complete. Not quite. It can be Turing complete as long as you fill in the proof steps the compiler can't infer for itself. Coq, Idris and other theorem provers can all produce programs with arbitrary looping behaviour given valid proofs are generated.
- dllthomas 5y agoThis 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?