when a computer algebra program (e.g., Mathematica) simplifies an expression, let it optionally emit a formal proof of the simplification which can be checked by an independent proof assistant program. the formal proof may be ugly and messy; it is intended only to be processed by a machine.
make formal methods widely used and available.
No comments :
Post a Comment