Re: Proofs, was Are there different programming languages that are compiled to the same intermediate language?

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.

Return to the comp.compilers page.
Search the comp.compilers archives again.