There are tools and programming language that are already way ahead of what you are describing. Examples are Idris, F* (F-Star), Dafny etc. They use Dependent Types and/or Refinement Types to make it possible to prove your code correct. There is now proven correct code in the Windows Kernel and other large projects implemented with those tools.