Comment by smaudet

> You still write the tests in standard Ruby and synthesized code should satisfy the logic as checked by the tests.

I think its important that the code still be user-modifiable:

Take this function, y = 2 * x.

Write a test, which proves for all real numbers, that y = 2 * x.

Can't do it, can you?

Tests can't fully specify code - this effort is doomed to be incomplete.