Hacker News new | past | comments | ask | show | jobs | submit login

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.

No. 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.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact