> A study of program structure had revealed that programs —even alternative programs for the same task and with the same mathematical content— can differ tremendously in their intellectual manageability. A number of rules have been discovered, violation of which will either seriously impair or totally destroy the intellectual manageability of the program. These rules are of two kinds. Those of the first kind are easily imposed mechanically, viz. by a suitably chosen programming language. Examples are the exclusion of goto-statements and of procedures with more than one output parameter. For those of the second kind I at least —but that may be due to lack of competence on my side— see no way of imposing them mechanically, as it seems to need some sort of automatic theorem prover for which I have no existence proof. Therefore, for the time being and perhaps forever, the rules of the second kind present themselves as elements of discipline required from the programmer. Some of the rules I have in mind are so clear that they can be taught and that there never needs to be an argument as to whether a given program violates them or not. Examples are the requirements that no loop should be written down without providing a proof for termination nor without stating the relation whose invariance will not be destroyed by the execution of the repeatable statement.
Interestingly, designing a language that enforces that loops need an invariant that proves they terminate is actually possible; Coq, for example, does pretty much exactly this from what I understand. My understanding is that this means that it isn't Turing complete, but I also think that maybe Turing completeness isn't quite as necessary for as many things as it might otherwise seem like.
Invariant is the property that is preserved on every iteration.
Proof of termination in imperative languages can be done by proving that a natural number decreases with every step.
Dafny implements this at the compiler level (and a curly braces syntax!).
Coq uses other methods more tailored towards recursion.
You are right that if every loop must terminate, it is not Turing complete.
So some valid programs will not compile.
There are some interesting programs that potentially never terminate (like servers, daemons, OS, games, etc) formal methods can be applied too. For instance to prove that they preserve certain property or that they don't terminate or terminate only under certain conditions.
I find the theory extremely elegant and pleasurable, but it´s obviously not everyone's cup of tea, as shown by its lack of widespread use.
LLM's might create a revival in the coming years for the following reasons:
1) cost of formalization goes down
2) cost of proving goes down
3) cost of programming goes down
4) provable code quality becomes a differentiation among a sea of programs
Interestingly, designing a language that enforces that loops need an invariant that proves they terminate is actually possible; Coq, for example, does pretty much exactly this from what I understand. My understanding is that this means that it isn't Turing complete, but I also think that maybe Turing completeness isn't quite as necessary for as many things as it might otherwise seem like.