I don't despair, because I know that to prove correctness of a program you need to use math.

For example proof assistants(like Coq, Agda, Idris, hol) are capable of proving correctness of a program.