People are under the impression that
not being Turing complete is somehow enough to be feasibly verifiable. If we place (realizable) computational models on a scale, with 0 being no computation at all, and 10 being Turing completeness, then the computational models we can generally verify are somewhere between 0 and 1 (with 1 being, say, FSMs). A language with no loops, no recursion and just subroutines and binary variables -- i.e. it's an FSM -- is already PSPACE-complete to verify, meaning we can only verify only very short programs in that language. In other words, you need to get
very far from Turing completeness to be generally verifiable.
This is why in general software verification doesn't try to come up with languages where all programs are verifiable, but aims to verify specific programs, sometimes regardless of the computational strength. Some programs in Turing complete languages can be verified (but certainly not all), just as some programs in FSM-strength languages can be verified (but certainly not all).
While it is certainly possible that a much bigger subset of, say, FSM programs can be verified than a subset of programs in TC languages, placing the bar at "Turing complete" is somewhat of a red herring.
Indeed, the LANGSEC link in the post[1] seems to understand that, noting that even verifying PDAs is undecidable, but it fails to note that even decidable verification tasks (for FSMs) are very often intractable, which -- for all practical purposes -- is just as bad as being undecidable.
[1]: http://langsec.org/occupy/