|
|
|
|
|
|
by todd8
991 days ago
|
|
|
I understand that modern type systems can do anything (that can be computed) since they are Turing complete. So are Java generics and C++ templates and Lisp’s macro systems, but I don’t want these things. I’ve written a number of Turing machine programs; yeah it’s impressive that an imaginary machine that is so simple can run any program that runs on any other computer, but it’s no fun writing code for a Turing machine. For the Theory of Computing studying Turing machines is important. If I don’t want Turing complete type systems, what do I want? Well, first off, the bugs I find in my programs that are more troubling don’t seem to be stopped by strong type systems. What I want is to be able to declare assertions in my code. For example, I’d like to tell the compiler that the variable year must always satisfy (2000 < year < 3000) and that in a certain block of code that x and y are always within 0.5 of each other. I want the compiler to ensure that these invariants are satisfied by a combination of compile time and run time checks generated by the compiler. The problem is that we can’t expect programmers to use Turing machine like type declarations, because the programmer must now program the type system without bugs to ensure that the types in the program carry enough information that higher level assertions can be made about the original program’s correctness. TLDR, I want to work with higher level assertions about the code than that provided by complex types. |
|
|
> A Turing machine is not "so simple that it can run any any program ...".
Simplicity has nothing to do with it. Turing showed that some very simple machines can calculate recursive functions.
Not every machine that is Turing Complete looks like a tape machine from Turing's papers.
> it's no fun writing code for a Turing machine
Almost every general-purpose programming language is a Universal Turing Machine; so that's like saying it's not fun to write code, period.