> 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.
The space of inputs and outputs is infinite. You can't prove programs are the same by "just" testing a bunch inputs.
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)