Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting proble

Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting problem". However, this doesn't mean we can't prove anything. Wikipedia says: > In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable. I often feel like the "trick" is to push the trivial stuff to be as useful as possible. You can work from several vectors: 1. You build better static analyzers (difficult and computationally expensive the further you push it - but that's what we're doing) 2. reduce the complexity of the "analyzed thing" (high level language, assembly,...) to allow for easier analysis, while still being useful (a assembly language only supporting 'nop' is trivial to analyze, but pretty useless overall; otoh you can disallow some constructs in C to make the language easier to analyze). There are of course other forms of "provably correct". E.g. programming in a language that has proofs attached to it, like coq [which is the name of a proof assistant]. Disclaimer: I've never used coq myself, but know plenty who do. I think that's something that might interest you. [And thanks to the genius who christened that tool: No, seriously, I'm not trying to be rude!] [edit] Didn't check that link, but maybe you find it interesting https://www.cs.princeton.edu/courses/archive/spring13/cos510/sf/Basics.html https://www.cs.princeton.edu/courses/archive/spring13/cos510... There are of course other approaches than coq, e.g. Isabelle is often mentioned. See the "See also" on https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq