The gap is IDEs becoming automated theorem provers. You put in the type signature of what you want and keep adding unit tests until the IDE finds the correct code for you.
Their philosophy are completely different. Formal proofs aim at proving the nonexistence of bugs, while tests (any kind of them) aim at revealing bugs in case you add them.
You can sometimes generate code form a proof, but you can't do that from tests.
