Comment Re:Particular (Score 2) 550
You may not be able to just take any program and prove that it works, but you can construct a program of your own in a way that it is possible to prove that it works; actually what you do is the proof and then in best-case scenario extract the machine code from that.
Of course, doing this is still very costly: 7500 lines of C-code can take 200000 lines of Isabelle proof code: