Correct, you cannot prove everything. But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" w

Correct, you cannot prove everything. But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" we manage to formally specify), and those we can't prove correct can probably be transformed into provable versions —assuming they're short enough.