As the cost of bugs and failures in systems increase as we rely more on code, the need to understand proof-checkers and formal verifiers is essential as we shift from a move-fast-and-break-things paradigm.
Here is my take on it, discussing how proof checkers leverage the Curry-Howard isomorphism and showing how to make a formal proof verifier yourself