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 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 14:25:56 -0700 Organization: A noiseless patient Spider Message-ID: <87o9idsh7f.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> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="c64f90128f27b36aa0215bf95afe8b2a"; logging-data="26602"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/CGAbTHTHNXXdaBqve/tam" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:Ci8xL1y6jfGnzXomytafsb1i/zw= sha1:HKf8td0V73agWS7TQmmqk/xDeQ0= Xref: reader02.eternal-september.org comp.lang.ada:51652 Date: 2018-04-20T14:25:56-07:00 List-Id: 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. Why do you say that? Even for ordinary testing, not extraordinary? 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. 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. 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. 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.