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

From	Spiros Bousbouras <spibou@gmail.com>
Newsgroups	comp.compilers
Subject	Re: Proofs, was Are there different programming languages that are compiled to the same intermediate language?
Date	2023-02-05 19:23 +0000
Organization	A noiseless patient Spider
Message-ID	<23-02-023@comp.compilers> (permalink)
References	<23-02-005@comp.compilers> <23-02-020@comp.compilers>

Show all headers | View raw

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.

Back to comp.compilers | Previous | Next — Previous in thread | Find similar

Thread

Re: Are there different programming languages that are compiled to the same intermediate language? Martin Ward <mwardgkc@gmail.com> - 2023-02-02 15:44 +0000
  Re: Are there different programming languages that are compiled to the same intermediate language? arnold@skeeve.com (Aharon Robbins) - 2023-02-03 08:26 +0000
  Re: Are there different programming languages that are compiled to the same intermediate language? anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-05 17:59 +0000
    Re: Proofs, was Are there different programming languages that are compiled to the same intermediate language? Spiros Bousbouras <spibou@gmail.com> - 2023-02-05 19:23 +0000

csiph-web