> Programming is significantly easier... because of things like syntax checking and compiler/interpreter errors. People[0][1] are using theorem provers to help

> Programming is significantly easier... because of things like syntax checking and compiler/interpreter errors. People[0][1] are using theorem provers to help teach students the general structure of a proof. And this is a bit of a tangent, but if you want to mess around with very simple proofs in first-order logic, the Open Logic Project[2] has an online proof editor and a textbook. [0]: https://link.springer.com/content/pdf/10.1007/s40753-021-00140-1.pdf https://link.springer.com/content/pdf/10.1007/s40753-021-001... [1]: https://xenaproject.wordpress.com/category/learning-lean/page/2/ https://xenaproject.wordpress.com/category/learning-lean/pag... [2]: https://proofs.openlogicproject.org/ https://proofs.openlogicproject.org/