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!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Wed, 06 May 2015 15:10:48 -0700 Organization: A noiseless patient Spider Message-ID: <87wq0l1hnb.fsf@jester.gateway.sonic.net> References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: mx02.eternal-september.org; posting-host="22184b02e80198190244f5a2dd813f11"; logging-data="14838"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1//r/4shXtxFsAIovsyK9Zt" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) Cancel-Lock: sha1:4rq948njYSbztLiKi4+sEn+Dtf8= sha1:/1Xuh91Qv6hWX8E4cyeJi0toJZk= Xref: news.eternal-september.org comp.lang.ada:25743 Date: 2015-05-06T15:10:48-07:00 List-Id: "Randy Brukardt" writes: > Lastly, fancy proof languages tend to be beyond the skill level of ordinary > (and some not so ordinary) programmers. Despite, 6 years of University > education, a masters degree, and 30 years of real-world experience, I had to > have both the meaning of the implication operator and a "universally > quantified predicate" explained to me. As it turns out, I had run into both > in the past, but not under those names. I'd say there's two rather different approaches to verified software: the approach based on Hoare logic (the precondition/postcondition stuff as used in SPARK); and the approach based on dependent types, as used in Coq. Dependent types are the idea that you can have a typed lambda calculus where the types are arbitrary predicates including quantified ones involving other terms. So if you have a term of a given type, that constitutes a constructive proof of a value of that type. By typechecking the term and then compiling it into code, you have a verified program that meets the specification expressed in the type. The two approaches came out of different traditions so they tend to use differing vocabulary (the stuff about quantified predicates is from mathematical logic) but it's not that big a deal. It sounds like you're more familiar with the SPARK approach than the Coq approach, but I think it's good to have some knowledge of both. Note that dependent types can be arbitrary complicated, e.g. a Coq type can express the execution semantics of a chunk of program code. If you can take a chunk of C code, assign semantics to it and label them with a type, and transmogrify the C code until it's a chunk of assembly code whose semantics have the same type as the C code as validated by a typechecker, then you have a verified compiler. This is basically how CompCert (compcert.inria.fr) works. The typechecker verifies that the compiler output has preserved the meaning of the input source code. You might like the online book "Software Foundations", which explains writing verified code in Coq: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html CompCert is one of Coq's success stories so Coq should be of considerable interest to people interested in formal verification. The book looks pretty accessible and working through it has been on my infinite TODO list for quite a while.