3 ms·
> 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" testin
by mahogany 3mo ago
> 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.
- nextaccountic 3mo agoIndeed. 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)