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 03:27:06 -0700 Organization: A noiseless patient Spider Message-ID: <8736zqkwat.fsf@nightsong.com> References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <878t9nemrl.fsf@nightsong.com> <87h8o7lowg.fsf@nightsong.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="c64f90128f27b36aa0215bf95afe8b2a"; logging-data="28121"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX190bGFMVVMrfMhTHjqC++qS" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:YaIHfYOu3l35X7WENq3AivbF+ww= sha1:yOd6PZ3+rSa3Y5YbZCmv+EYTmNE= Xref: reader02.eternal-september.org comp.lang.ada:51641 Date: 2018-04-20T03:27:06-07:00 List-Id: "Dan'l Miller" writes: > Coq is increasingly setting its sights on the wild-west worlds of C > and machine code: [links] Thanks, yes, I had seen some of those, will look at the others. But, it's a niche area. Most programmers I meet these days have never written anything in C or machine code. Realtime programming in general is a niche area: most programmers I know have never done any. Critical systems are also niche, and realtime critical systems are the most niche of all. And finally I don't know whether BIG critical realtime systems exist at all; and if they do, whether they could be split up. Ada, especially with high-end verification methods, is about the intersection of it all, i.e. critical AND hard-realtime AND large. Those are intense requirements and it takes a lot of work to satisfy them. If you aren't faced with those requirements, why do all that work? Non-realtime means you can use arbitrary precision arithmetic (eliminating all those proofs about integer overflow) and garbage collection (automating memory management). Realtime but non-critical means you can get adequate reliability from traditional software testing instead of proof systems. Realtime and critical, but not too large, means you can jettison a lot of Ada's features and work with a much more tractable subset (e.g. the original SPARK). "Crossing the chasm" gives a picture of a large set of problems for which Ada is the best solution, where the challenge is getting people to appreciate this fact. But I'm having trouble seeing the large set of problems, especially once formal verification is part of the prescription: - If the problem is not realtime, it's probably easier to use a garbage collected language instead of Ada. Realtime is a niche area of programming, so even if Ada completely takes it over, the "chasm" between Ada and the wider programming world is not even slightly crossed. - If the problem is not critical (human safety is not endangered, and mistakes aren't enormously expensive to repair), then at least for now, verification is still much harder than ordinary testing. If you're proposing making verification as easy as testing, that's great, but it's a mammoth research problem rather than a matter of straightforward advocacy or tool development. - A lot of not-so-critical realtime code is being written in C (e.g. on embedded MCUs in consumer electronics). I'd agree that we're probably better off if that stuff was instead done in Ada, with or without formal verification. - Finally I think there are realtime problems like bit-banging comms protocols that might have been done with software back in the day, but that now get done with FPGA's (i.e. in VHDL or Verilog) now that FPGA's are cheap, since it's much easier to get deterministic timing with FPGA's than with CPUs. So a fair number of applications have actually been removed from Ada's problem space. > defines Ada's language semantics in English prose that compiler > vendors cannot take as direct input into their compiler > implementations. Yes, this is an area where mechanized semantics would be a big win. They had to do that for C in order to write CompCert. You might look at Twelf which is designed for such purposes. > Speaking of SPARK, here is SPARK-esque analogue for a subset of C++: > http://EscherTech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf Thanks, this is interesting.