From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,LOTS_OF_MONEY autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: How to get Ada to =?utf-8?Q?=E2=80=9Ccross?= the =?utf-8?Q?ch?= =?utf-8?Q?asm=E2=80=9D=3F?= Date: Fri, 20 Apr 2018 17:10:02 -0700 Organization: A noiseless patient Spider Message-ID: <87k1t1s9lx.fsf@nightsong.com> References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <878t9nemrl.fsf@nightsong.com> <87h8o7lowg.fsf@nightsong.com> <8736zqkwat.fsf@nightsong.com> <6839088c-f221-4650-a6ea-1841ae539486@googlegroups.com> <1e5f5681-0e2a-43cc-9437-2bd38078da08@googlegroups.com> <87604lvkqp.fsf@nightsong.com> <0bd80336-595a-45b6-b4e5-26c13d5859cb@googlegroups.com> <87o9idsh7f.fsf@nightsong.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="532e8b2aa0bc5beb3e34e3489a7ffcd6"; logging-data="17586"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18po7625VR55Z90E3iApnBd" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:Tr1uxSNcWXjmW1X/4DM8sblDRA0= sha1:7YAOHlPHvxxtlkgh9TUcunPu5L4= Xref: reader02.eternal-september.org comp.lang.ada:51654 Date: 2018-04-20T17:10:02-07:00 List-Id: Shark8 writes: >> Why do you say that? Even for ordinary testing, not extraordinary? > Meltdown and Spectre -- which stem from caching and speculative execution. What does that have to do with anything? > It's about the *properties* here, not just whether "A:= 1 + A;" > correctly generates an increment, or whether it can overflow. I can't tell what you mean by this. I may be missing something basic. > In such an IDE the VHDL has to have some manner of proving properties; That sounds like you're talking about proofs embedded in the VHDL code, that prove SPARK-like VC's about the circuit being described. That's fine and necessary. But the topic I asked about is the proofs used in the compiler, not the proofs embedded in the compiled program. > Never crashing is a good thing; it's far better to have a controlled > exit than possibly leave things in a inconsistent state. 1. Of course it's a good thing, but is it CRITICAL? For a jet engine it is critical. For a compiler I'm claiming it's not critical. I'm open to persuasion but at the moment I don't see the other side. Let's put it another way: you are running a crashfree compiler when a mischievous billionaire offers you $10 million if you let him smash your computer with a sledgehammer (setting you back a day or so while you buy a new computer and restore your backups to it). If you take the $10 million, I claim you would have been ok without the crashfree compiler. 2. What inconsistent state is left if the compiler crashes? It's just a usermode program. There's an error message saying that the compiler crashed, and hopefully some diagnostic info saying how the crash happened. 3. There are many ways compilation can fail, even if the compiler software is perfect, such as a power failure in the office, problems with the computer hardware, the building being hit by a meteor or tsunami, or the above-described mischievous billionaire showing up. At a typical office there's maybe 1e-3 chance that one of those things happens on a given day (the billionaire is the least likely of course), With a well-tested compiler (verified like CompCert, but not SPARK verified), you have at worst 1e-6 chance of hitting an input that it can't compile (you get an error message instead, not wrong code). How much are you willing to pay to decrease the 1e-6 to 1e-10 by using SPARK? If the amount is more than zero, what are you doing about the 1e-3 chance of other problems? Anyway, you have not explained how it's even conceptually possible to write a SPARK verified Ada compiler that compiles every possible Ada program, rather than a restricted subset. If there's a VC requiring the compiler to never use more than N bytes of memory, then what do you do with an input that uses N+1 levels of nested parentheses (rejecting it and printing an error message is no different than crashing and printing an error message)? If there's not such a VC, how can you guarantee that your compiler never crashes from memory exhaustion? Really, SPARK is great, but I think I'm seeing some overreaching claims for it in this thread.