Path: csiph.com!weretis.net!feeder6.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end From: Spiros Bousbouras Newsgroups: comp.compilers Subject: Re: Proofs, was Are there different programming languages that are compiled to the same intermediate language? Date: Sun, 5 Feb 2023 19:23:36 -0000 (UTC) Organization: A noiseless patient Spider Sender: johnl@iecc.com Approved: comp.compilers@iecc.com Message-ID: <23-02-023@comp.compilers> References: <23-02-005@comp.compilers> <23-02-020@comp.compilers> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Injection-Info: gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="32614"; mail-complaints-to="abuse@iecc.com" Keywords: theory Posted-Date: 05 Feb 2023 14:25:47 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com X-Server-Commands: nowebcancel X-Organisation: Weyland-Yutani In-Reply-To: <23-02-020@comp.compilers> Xref: csiph.com comp.compilers:3367 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.