Is there a difference here between a proof and an automated test?
I'm curious what a proof would look like compared to my RSpec unit tests and what the actual implementation would look like.
A test tests some - but not all - of the paths through your code. And some - but not all - of the inputs you might see.
A proof establishes that your code works correctly on all paths, inputs, etc.
A test tests some - but not all - of the paths through your code. And some - but not all - of the inputs you might see.
A proof establishes that your code works correctly on all paths, inputs, etc.