On Sun, 05 Feb 2023 17:59:03 GMT
anton@mips.complang.tuwien.ac.at (Anton Ertl) wrote:

2) A program has to satisfy the requirements of its users, while a
published proof is limited to proving a published theorem. One
example of the difference is that undefinedness is totally acceptable
in mathematics, while it is a bug in programs

All programmes have de facto limitations in the input they can process correctly imposed by the hardware , operating system , etc. If they advertise that they will detect some kind of invalid input and fail to do so , that's a bug. If they make no such claims then it boils down to whether one can "reasonably" expect the programme to detect the invalid input and report it but what counts as reasonable will generally be a matter of dispute. Note also
that there can be grey areas. For example a numerical analysis programme may produce for some range of inputs an output which is not 100% correct but
"close enough". But what's close enough depends on many factors.

(interestingly, there is
a significant number of compiler writers who take the mathematical
view in what they provide to programmers, but consider that a program
in their programming language that exercises the undefined behaviour
that they provide to programmers to be buggy).

This is a cryptic comment. To the extent that I can guess from knowing
about your pet peeves what you're talking about , I don't think what
you say describes the views of compiler writers.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)