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 capab

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.