I think Robert Martin doesn't fully grasp the field of formal methods and program semantics, which has evolved a lot since the early 1980s. Paraphrasing Alan Pe

I think Robert Martin doesn't fully grasp the field of formal methods and program semantics, which has evolved a lot since the early 1980s. Paraphrasing Alan Perlis, beware of the Turing tar pit, where everything is possible but nothing of interest is easy. So one trick is to work on DSLs with restricted semantics that are good enough for your domain. That makes proofs plus other formal techniques, and hence security guarantees, much much easier. But if you insist on Turing complete languages, as I explained above, you can e.g. build abstract interpreters or data flow analyses that are able to prove really sophisticated things. I have implemented a C abstract interpreter for an industrial client that among many other things detected whether you were making potential out of bounds accesses to arrays, or potentially using uninitialized pointers. Of course it erred on the safe side. But it was really precise (few false positives). Not a walk in the park as it relies on Galois connections. See the seminal Cousot & Cousot 1977 paper [1]. [1] https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml