This chapter explores the landscape of proof assistants and programming languages, focusing on the desire for verification and implementation correctness. It contrasts existing systems with Metamath, highlighting its efficiency, simplicity, and educational value. The discussion also addresses the challenges posed by dependent type theory and the usability of SMT solvers in the context of program verification.