cvoss, ezwoodland, tromp and v64 made a good point. As v64 points I was thinking of a Combinatory Completeness not Turing Completeness. Dropping that requirement as cvoss, ezwoodland, tromp point you can simulate deletion (that's what quantum computing does btw see No-deleting theorem).
> The decline in allocative efficiency should be more of a main focus — we need to throw more of our intellectual capital at understanding how to increase competitiveness and the market potential for innovative firms and technologies, in the same way that we've focused on understanding how to make better technologies.
I love programming as theory building. One key thing: if the program is built for a business then the theory must revolve around the business. For example, it should include things as "easiness to hire devs for this code base”, "stability of current business model” and “how important each feature is for the business”.
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
I’m working on old fashioned A.I. for my PhD. I wrote Doug a few times, he was very kind and offered very good advice. I was hoping to work with him one day.
I see the endgame now, thanks guys.