2 ms·
But it seems to me that the fact that they have a theorem prover at all means they do know ahead of time what semantic preserving transformations are available.
by bloaf 10y ago
But it seems to me that the fact that they have a theorem prover at all means they do know ahead of time what semantic preserving transformations are available.
- dom0 10y agoNo. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.