In fact, you can write proofs as programs. https://leanprover.github.io/ https://leanprover.github.io/ - Lean, very popular proof assistant from Microsoft. The

In fact, you can write proofs as programs. https://leanprover.github.io/ https://leanprover.github.io/ - Lean, very popular proof assistant from Microsoft. There are tons information on it on youtube. Another good paper to look at is `How to Write a Proof` by Leslie Lamport http://lamport.azurewebsites.net/pubs/lamport-how-to-write.pdf http://lamport.azurewebsites.net/pubs/lamport-how-to-write.p... There he argues that mathematical proofs should be written and structured like software code. Leslie came up with TLA+: http://lamport.azurewebsites.net/tla/tla.html?from=https://research.microsoft.com/users/lamport/tla/tla.html&type=path http://lamport.azurewebsites.net/tla/tla.html?from=https://r... It can be used to write a proof that algorithm is correct. AWS uses it: https://lamport.azurewebsites.net/tla/amazon-excerpt.html https://lamport.azurewebsites.net/tla/amazon-excerpt.html All the important distributed algorithms were formally verified using proof assistants. The entire field of "formal verification" is nothing but writing proofs to verify correctness of software & hardware. There are tons of lectures on formal verification.