Is it feasible or even possible to use relational algebra and/or relational calculus in the form of proofs to test/verify the correctness of SQL statements, functions, and stored procedures?
It seems to me like it should be at least possible, but I don't know if there's a detail I'm missing that makes a 1:1 mapping between the proof and the code incorrect.
Have any of you tried a method like this? Did it work? What were your experiences like?