3 ms·

To expand on the why: They are the theoretical foundation for imperative/procedural programming. Things like assembly or C would not exist without Turing machin

To expand on the why: They are the theoretical foundation for imperative/procedural programming. Things like assembly or C would not exist without Turing machines. The only other influential, foundational turing-complete language is Church's lambda calculus, which is much nicer to reason about and led to the development of functional programming. In fact, comparing Turing machines and Lambda calculus gives you an approximation of how much easier functional programs are to write (provably) correctly than more conventional ones.

User23 7y ago
With discipline and the proper application of the predicate calculus it's no harder to write provably correct imperative programs than it is functional ones. I'm most familiar with the work of Dijkstra and Scholten, but I'm certain that Hoare, Lamport, and many others have made great use of the technique or very similar ones. Note that this method is not proving the correctness of arbitrary programs, it is deriving programs that must be correct because of the way in which they were written. The introductory paper[1] is readable and short and I recommend anyone interested read it. That said, since in this case one is working with predicate transformers, which are mathematical objects, perhaps one can support the claim that it's just applying functional methods to imperative programming. I'm not so sure, but in the end it's not very important to me either way. I just like knowing that I have strategies for writing good programs be they functional or imperative. This does make me doubt the practical usefulness of the Turing machine model for the professional software engineer though. I'm not aware of any technique that derives nontrivial correct programs using Turing machines. While the most formal predicate transformer based approaches are relatively rarely used and only for the trickiest problems, anyone who is familiar with both will recognize that properly applied TDD is extremely similar, so much so that I consider it a sufficiently rigorous informal approximation for the vast majority of practical cases. [1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD472.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD472...

User23 7y ago

With discipline and the proper application of the predicate calculus it's no harder to write provably correct imperative programs than it is functional ones. I'm most familiar with the work of Dijkstra and Scholten, but I'm certain that Hoare, Lamport, and many others have made great use of the technique or very similar ones. Note that this method is not proving the correctness of arbitrary programs, it is deriving programs that must be correct because of the way in which they were written. The introductory paper[1] is readable and short and I recommend anyone interested read it. That said, since in this case one is working with predicate transformers, which are mathematical objects, perhaps one can support the claim that it's just applying functional methods to imperative programming. I'm not so sure, but in the end it's not very important to me either way. I just like knowing that I have strategies for writing good programs be they functional or imperative. This does make me doubt the practical usefulness of the Turing machine model for the professional software engineer though. I'm not aware of any technique that derives nontrivial correct programs using Turing machines. While the most formal predicate transformer based approaches are relatively rarely used and only for the trickiest problems, anyone who is familiar with both will recognize that properly applied TDD is extremely similar, so much so that I consider it a sufficiently rigorous informal approximation for the vast majority of practical cases. [1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD472.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD472...