PBT were introduced by John Hughes and Co° back in 1993, I am not sure how “today” is better than 20 years ago on that matter. And no, PBT cannot prove anything. Once again, consider currency exchange. 200 currencies. 40K pairs. For some the rate is to be calculated through crossing. For one combination it’s failing. THere is no way on the Earth one come up with tests to cover this particular case.
It’s not a test suite per se (although it could be.) Cure just produces BEAMs so it stays in the compilation chain. Lean4 is something one is to run ad-hoc.
