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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:b95d:: with SMTP id k29-v6mr2663709iti.6.1524264549127; Fri, 20 Apr 2018 15:49:09 -0700 (PDT) X-Received: by 2002:a9d:70d7:: with SMTP id w23-v6mr152652otj.3.1524264548663; Fri, 20 Apr 2018 15:49:08 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!feeder.erje.net!2.eu.feeder.erje.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!f63-v6no1272773itc.0!news-out.google.com!u64-v6ni2265itb.0!nntp.google.com!k65-v6no1263090ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 20 Apr 2018 15:49:08 -0700 (PDT) In-Reply-To: <87o9idsh7f.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.113.16.86; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 76.113.16.86 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> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: =?UTF-8?B?UmU6IEhvdyB0byBnZXQgQWRhIHRvIOKAnGNyb3NzIHRoZSBjaGFzbeKAnT8=?= From: Shark8 Injection-Date: Fri, 20 Apr 2018 22:49:09 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 5226 X-Received-Body-CRC: 3903951160 Xref: reader02.eternal-september.org comp.lang.ada:51653 Date: 2018-04-20T15:49:08-07:00 List-Id: On Friday, April 20, 2018 at 3:25:58 PM UTC-6, Paul Rubin wrote: > Shark8 writes: > >> If you use CompCert's approach (use recursion and unbounded arithmetic > >> and automatic memory management in the compiler as much as you want, > >> prove that the compiler won't generate bad code, use ordinary software > >> testing to give reasonable assurance that the compiler doesn't crash, > >> and call it a day) you can probably save a heck of a lot of work. > > > > "Extraordinary testing" simply isn't good enough. >=20 > Why do you say that? Even for ordinary testing, not extraordinary? Meltdown and Spectre -- which stem from caching and speculative execution. It's about the *properties* here, not just whether "A:=3D 1 + A;" correctly= generates an increment, or whether it can overflow. > The testing is not to protect against wrong-code generation since the > theorem prover does that. The testing only gives some assurance (the > same level that you get from normal commercial software, i.e. not > mathematical proof but reasonable practical confidence), that the > compiler won't do something like crash from a memory leak. Again; not sufficient. In such an IDE the VHDL has to have some manner of proving properties; whic= h SPARK does do (a lot of your cited VCs, like lack of overflows, are there= because they invalidate properties that need to hold). > That means that the compiler is allowed to use garbage collection, as > CompCert does. It makes writing the compiler much easier. I think > SPARK programs are not allowed to use garbage collection because SPARK > has to guarantee that the programs never crash. Never crashing is a good thing; it's far better to have a controlled exit t= han possibly leave things in a inconsistent state. > A compiler is not like a jet engine controller. If it generates wrong > code, that's potentially disastrous. But if it doesn't work at all, > that's only annoying. You need SPARK for the jet engine controller > because it HAS TO WORK or the plane stops flying and people die. If the > compiler doesn't work, you lose a little bit of development time filing > a bug report with the maintainers and finding a workaround. Except we're also talking about the possible production of chips via VHDL; = something like, oh, a pacemaker ASIC or a microcontroller for automotive-us= e... say in the braking or throttle system. As such, it *SHOULD* be treated as a critical system: it's not just SW that= you can hot-patch, it's also etched HW that is essentially set in stone. S= o, yes, it should be provably correct. > Therefore, verifying a compiler with SPARK (which means giving up > garbage collection and arbitrary-precision integers, instead making > yourself satisfy a lot of verification conditions about not overflowing > machine-width integers) seems like a waste of effort. All you really > care about is not getting wrong code. You can accept a low probability > of outright failure to not generate any code at all. Except you're flat-out wrong; the system needs to be provable, not just in = correctness but in the properties of the underlying constructs. It needs to be a system where, upon submission of a "project" the compilati= on-result is either "success, and provable from source to object", or "Erro= r, because of XXX." -- Where XXX is something like "inputs exceeded working= memory" or "could not prove properties Y & Z." or "Semantic-error, violati= on of LRM N.N.N." or the like. -- There should be no "low probability of fa= ilure".