On 13/07/2020 15:03, Peter Bishop wrote: > <snip? > Plus, even if we could prove all this, "correct" in this sense does not > mean that > the specified behaviour is actually what is needed for the application. > Correct (no irony intended). Olwen