Based on the halting problem, a provably complete analysis of the behavior of some (most?) programs in a turing-complete language is impossible. To put it another way, it is impossible to be sure that there isn't another vulnerability after you've patched the last one.
I don't own any crypto assets myself, but I think that using a non-turing-complete scripting language for the bitcoin blockchain was a wise decision rather than a lack of vision.
The halting problem doesn't say that you can't do a complete analysis of a PARTICULAR program to see if it halts, it just says you can't have a general algorithm that would do this for ALL programs.
Since we are trying to analyze particular programs, you aren't going to be limited by the halting problem.
If it's possible to do a complete analysis of any particular program, shouldn't it follow that it's possible to do a complete analysis of all programs?
If only a subset of all programs can be completely analyzed as particular programs, what are the boundaries of that set?
So the halting problem isn't stating that there exists a program that you can't analyze to see if it stops, the problem states you can't create a single PROGRAM that will be able to analyze all other programs.
A very crude explanation for the proof is something like this:
Imagine you design a program that takes another program as input and tells you if it halts.
Now, imagine you create another program, and all it does is call your first program, passing itself as the argument. Then, it does the opposite of whatever the first program predicts that it will do; if your 'halting detection program' says this new program will halt, the program instead loops forever. If your 'halting detection program' says this new program will loop forever, instead it halts.
So, in short, the idea is that you can't create a program IN ADVANCE that can't be tricked by a future program that knows about the halting detection program you are using.
So yes, you CAN analyze any program, but not by using a single algorithm.
I'm familiar with the proof and the story.
My point is that the claim that any particular program can be fully analyzed is equivalent to saying that all programs can be analyzed.
Perhaps you're saying that it's possible to analyze any particular program for known exploits once they've been discovered?
Take the set of all finite C programs without loops or recursive function calls. They (clearly?) halt.
Or: the set of all finite Brainfuck programs that don't contain a `[` or `]` instruction. Those also halt.
Also, see Idris: https://www.idris-lang.org/. It's a language that has dependent types and a totality checker.
A dependent type is a value which depends on another value. For example, the length of an array depends on how many elements there are in the array.
A totality checker means that you must prove that a program that you write halts; otherwise, it fails to compile.
In Idris, if you ever write the equivalent of reduce recursively, you must prove that the recursion will terminate. This is done by noting that the length of an array is dependent on how many elements are in the array, noting that if an array has zero length then reduce will terminate, and noting that every time reduce is called with a non-zero array length it returns reduce called with that array length decremented by one. Then, since repeatedly subtracting one from a positive number eventually reaches zero (at which point the recursion halts) you're guaranteed that your reduce function halts.
EDIT: I guess you are right in the strict sense that languages like Idris aren't Turing complete. But they still can do a huge number of computable and useful things (and most of the things you'd want other languages to do), so I feel like "Turing complete" is mostly a semantic argument here.
In my mind it's more like an acceptable upper bound on provability of immutable and eternal transactions on some distributed machine. The downside to unexpected exploits far outweighs the upside to unlimited flexibility. Bitcoin chose a non turing-complete script for its transactions, and the short history of cryptocurrency has already prove that is much more secure than the infinite-possibilities of the Ethereum VM. Time will tell, but I personally expect "shocking" exploits of Ethereum smart contracts to continue ad-infinitum.
Perhaps there remains some unexplored region in the limited yet flexible yet verifiable space of languages that was until now uninteresting.
I wasn't claiming that it is not possible to analyze a program to detect known exploits. Rather that it is extremely probable that another exploit will be found after the last one has been patched, and it is impossible to prove otherwise.
The halting problem doesn't prevent playing whack-a-mole against previous exploits, but it ensures that proving more exploits do not exist is impossible. That's why I think a turing-complete language for smart contracts is a poor choice.
The first one stops. The second one does not. It's possible - trivial - to analyze them, but that doesn't tell you anything about whether all programs can be analyzed.
