> Just run both pgrust and postgres and compare the output.
The space of inputs and outputs is infinite. You can't prove programs are the same by "just" testing a bunch inputs.
> Just run both pgrust and postgres and compare the output.
The space of inputs and outputs is infinite. You can't prove programs are the same by "just" testing a bunch inputs.
Indeed. This approach is an improvement / augmentation over tests, not a panacea.
Neither postgres nor pgrust have their behavior specified using formal methods. (pgrust could write some contracts using something like kani or creusot, but having upstream postgres also write contracts is a tougher sell). If they had, one could write a giant proof that said the two software essentially do the same thing (at least in a subset of environments and some simplifying assumptions)