Re: [TUHS] TUHS Digest, Vol 33, Issue 5

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Noel Chiappa]

    > From: Steve Simon

    > well spec'ed machines where more common in the past.

Err, engineering data is not the same thing as a formal specification. If not,
almost every computer built could be said to have a 'formal spec' - there
usually are engineering documents for anything that was produced in any sort
of quantity.

Also, whether said engineering info is publicly available or not (which seems
to be another of your observations) is an orthogonal axis.

   Noel

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Bakul Shah]

On Aug 6, 2018, at 6:06 AM, Noel Chiappa <jnc@mercury.lcs.mit.edu> wrote:
> 
>> From: Steve Simon
> 
>> well spec'ed machines where more common in the past.
> 
> Err, engineering data is not the same thing as a formal specification. If not,
> almost every computer built could be said to have a 'formal spec' - there
> usually are engineering documents for anything that was produced in any sort
> of quantity.

What counts as a "formal spec"? Is it like Justice Potter Stewart's
"I know it when I see it" definition or something better?

> Also, whether said engineering info is publicly available or not (which seems
> to be another of your observations) is an orthogonal axis.

Agree.

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Hellwig Geisse]

On Mo, 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
> 
> What counts as a "formal spec"? Is it like Justice Potter Stewart's
> "I know it when I see it" definition or something better?
> 

For me, a "formal spec" should serve two goals:
1) You can reason about the thing that is specified.
2) The spec can be "executed" (i.e., there is an
   interpreting mechanism, which lets the spec behave
   like the real thing).

Hellwig

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Steve Johnson]

[-- Attachment #1: Type: text/plain, Size: 1338 bytes --]


I take a somewhat more relaxed view of what a spec should be:
It should describe a program with enough completeness that a competent
programmer could write it from the spec alone.
Each section of the spec should be capable of being tested.
If all the tests for all the sections pass, then the program is ready
for general use.

The formal systems I have seen would roll over and die when presented
with
even a simple compiler.  Additionally, being able to specify that a
particular
function be carried out by a heapsort, for example, would require that
the
formalism could describe the heapsort and prove it correct.  These
don't
grow on trees...

Steve

----- Original Message -----
From: "Hellwig Geisse" <hellwig.geisse@mni.thm.de>
To:<tuhs@minnie.tuhs.org>
Cc:
Sent:Mon, 06 Aug 2018 18:30:30 +0200
Subject:Re: [TUHS] TUHS Digest, Vol 33, Issue 5

 On Mo, 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
 > 
 > What counts as a "formal spec"? Is it like Justice Potter Stewart's
 > "I know it when I see it" definition or something better?
 > 

 For me, a "formal spec" should serve two goals:
 1) You can reason about the thing that is specified.
 2) The spec can be "executed" (i.e., there is an
    interpreting mechanism, which lets the spec behave
    like the real thing).

 Hellwig


[-- Attachment #2: Type: text/html, Size: 2159 bytes --]

[TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[Perry E. Metzger]

Sorry for the thread necromancy, but this is a _very_ important
topic. Perhaps it doesn't belong on tuhs but rather on coff.

This is a pretty long posting. If you don't care to read it, the TL;DR
is that formal specification and verification is now a real
discipline, which it wasn't in the old days, and there are systems to
do it in, and it's well understood.

On 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
>
> What counts as a "formal spec"? Is it like Justice Potter
> Stewart's "I know it when I see it" definition or something
> better?

At this point, we have a good definition. A formal specification is a
description of the behavior of a program or piece of hardware in a
precise machine-readable form that may be used as the basis for fully
formal verification of the behavior of an implementation. Often these
days, the specification is given in a formal logic, such as the
predicative calculus of inductive constructions, which is the logic
underlying the Coq system.

Isabelle/HOL is another popular system for this sort of work. ACL2 is
(from what I can tell) of more historical interest but it has
apparently been used for things like the formal verification of
floating point and cache control units for real hardware. (It is my
understanding that it has been many years since Intel would dare
release a system where the cache unit wasn't verified, and the only
time in decades it tried to release a non-verified FPU, it got the
FDIV bug and has never tried that again.) There are some others out
there, like F*, Lean, etc.

Formal specifications good enough for full formal verification have
been made for a variety of artifacts along with proofs that the
artifacts follow the specification. There's a fully formally verified
C compiler called CompCert for example, based on an operational
semantics written in Coq. There's another formal semantics for C
written in K, which is a rather different formal system. There's a
verified microkernel, seL4, whose specification is written in
Isabelle/HOL. There's a fully formal specification of the RISC V, and
an associated verified RTL implementation.

Generally speaking, a formal specification:

1) Must be machine readable
2) The semantics of the underlying specification language must
   themselves be extremely precisely described. You can't prove the
   consistency and completeness of the underlying system (see Gödel)
   but you _can_ still strongly specify the language.
3) Must be usable for formal (that is, machine checkable) proofs that
   implementations comply with the spec, so it has to be sufficiently
   powerful. Typical systems are now equivalent to higher order logic.

From: "Hellwig Geisse" <hellwig.geisse@mni.thm.de>
Sent:Mon, 06 Aug 2018 18:30:30 +0200
>
>  For me, a "formal spec" should serve two goals:
>  1) You can reason about the thing that is specified.

Yes.

2) The spec can be "executed" (i.e., there is an
>  interpreting mechanism, which lets the spec behave
>  like the real thing).

Not always reasonable.

First, it is often the case that a spec does not describe execution at
all. See, for example, the specification of a sorting function I give
at the end of this message: it simply says "a sorting function is a
function such that, for all inputs, the return is a non-decreasing
permutation of the input". This is not executable. It is a purely
descriptive property, and you cannot extract an executable algorithm
from the spec.

Second, even when a spec amounts to a description of execution, a
proof assistant often cannot actually execute it. For example,
although you can reason about non-terminating execution in pCiC (and
thus Coq), programs written in a strongly normalizing lambda calculus
that can be used as a logic must terminate, or functions that did not
terminate would be inhabitants of all types and the logic would be
inconsistent. Thus, you cannot execute a program with infinite loops
inside Coq, although you can reason about them (and indeed, you can
reason about coinductively defined objects like infinite execution
traces.)

On Mon, 06 Aug 2018 14:19:31 -0700 "Steve Johnson" <scj@yaccman.com>
wrote:
> I take a somewhat more relaxed view of what a spec should be:
> It should describe a program with enough completeness that a
> competent programmer could write it from the spec alone.

I think this is a bit more relaxed than is currently accepted.

> The formal systems I have seen would roll over and die when
> presented with even a simple compiler.__

I don't know what this means. If it is that there aren't
implementations of languages like pCiC, that's not true, see Coq. If
it means no one can formally specify a compiler, given that formally
verified compilers exist, that's also not true.

The "final theorem" proving the correctness of CompCert depends on
having an operational semantics of both C and the target architecture,
and says (more or less) that the observed behavior of the input
program in C is the same as the observed behavior of the output
program (say in ARM machine language). This is a serious piece of
work, but it is also something that has actually been done -- the
tools are capable of the task.

> Additionally, being able to specify that a particular function be
> carried out by a heapsort, for example, would require that the
> formalism could describe the heapsort and prove it correct.__ These
> don't grow on trees...

Formally verifying a couple of sorting algorithms described in Coq is
a exercise for an intro level class on formal verification. I've done
it. Once you have the proper primitives described, the specification
for a sorting algorithm in Coq looks like this:

Definition is_a_sorting_algorithm (f: list nat -> list nat) :=
  forall al, Permutation al (f al) /\ sorted (f al).

That says "the property "is_a_sorting_algorithm" over a function from
lists of natural numbers to lists of natural numbers is that the
output is a permutation of the input in which all the elements are in
non-decreasing order." The definitions in question are very
precise. For example, one definition of sorted (the property of being
a non-decreasing list) is:

Definition sorted (al: list nat) :=
 forall i j, i < j < length al -> nth i al 0 <= nth j al 0.

and the property of being a permutation, which is relatively
complicated inductively defined property, is:

Inductive Permutation {A : Type} : list A -> list A -> Prop :=
    perm_nil : Permutation
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' ->
                Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' ->
                 Permutation l' l'' ->
                 Permutation l l''.

Coq starts out with basically nothing defined, by the way. Notions
such as "natural number" and "list" are not built in. Peano naturals
are defined in the system thusly:

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

The underlying basis of Coq (i.e. the Predicative Calculus of
Inductive Constructions) is a dependently typed lambda calculus that's
astonishingly simple, and the checker for proofs in the system is only
a few hundred lines long -- the checker is the only portion of the
system which needs to be trusted.

In recent years, I've noted that "old timers" (such as many of us,
myself included) seem to be unaware of the fact that systems like Coq
exist, or that it is now relatively (I emphasize _relatively_) routine
for substantial systems to be fully formally specified and then fully
formally verified.


Perry
-- 
Perry E. Metzger		perry@piermont.com

Re: [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[George Michaelson]

Witness to this, the interest in *trying* to apply Coq to Ethereum
smart contracts...

I say "try" because as a complete skeptic, I think the attempt is
doomed except in very small sense. But the reason they are trying is
the importance to FinTech of formally verified state in the expression
of financial transactions. These are serious people. A bunch from
french academic research institutions, a bunch from the CSIRO in
Australia.

I think Perry wrote something of long term value. I encourage you to
write this up somewhere you'd be willing to have published like a tech
blog.

-G

On Sun, Aug 19, 2018 at 5:57 AM, Perry E. Metzger <perry@piermont.com> wrote:
> Sorry for the thread necromancy, but this is a _very_ important
> topic. Perhaps it doesn't belong on tuhs but rather on coff.
>
> This is a pretty long posting. If you don't care to read it, the TL;DR
> is that formal specification and verification is now a real
> discipline, which it wasn't in the old days, and there are systems to
> do it in, and it's well understood.
>
> On 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
>>
>> What counts as a "formal spec"? Is it like Justice Potter
>> Stewart's "I know it when I see it" definition or something
>> better?
>
> At this point, we have a good definition. A formal specification is a
> description of the behavior of a program or piece of hardware in a
> precise machine-readable form that may be used as the basis for fully
> formal verification of the behavior of an implementation. Often these
> days, the specification is given in a formal logic, such as the
> predicative calculus of inductive constructions, which is the logic
> underlying the Coq system.
>
> Isabelle/HOL is another popular system for this sort of work. ACL2 is
> (from what I can tell) of more historical interest but it has
> apparently been used for things like the formal verification of
> floating point and cache control units for real hardware. (It is my
> understanding that it has been many years since Intel would dare
> release a system where the cache unit wasn't verified, and the only
> time in decades it tried to release a non-verified FPU, it got the
> FDIV bug and has never tried that again.) There are some others out
> there, like F*, Lean, etc.
>
> Formal specifications good enough for full formal verification have
> been made for a variety of artifacts along with proofs that the
> artifacts follow the specification. There's a fully formally verified
> C compiler called CompCert for example, based on an operational
> semantics written in Coq. There's another formal semantics for C
> written in K, which is a rather different formal system. There's a
> verified microkernel, seL4, whose specification is written in
> Isabelle/HOL. There's a fully formal specification of the RISC V, and
> an associated verified RTL implementation.
>
> Generally speaking, a formal specification:
>
> 1) Must be machine readable
> 2) The semantics of the underlying specification language must
>    themselves be extremely precisely described. You can't prove the
>    consistency and completeness of the underlying system (see Gödel)
>    but you _can_ still strongly specify the language.
> 3) Must be usable for formal (that is, machine checkable) proofs that
>    implementations comply with the spec, so it has to be sufficiently
>    powerful. Typical systems are now equivalent to higher order logic.
>
> From: "Hellwig Geisse" <hellwig.geisse@mni.thm.de>
> Sent:Mon, 06 Aug 2018 18:30:30 +0200
>>
>>  For me, a "formal spec" should serve two goals:
>>  1) You can reason about the thing that is specified.
>
> Yes.
>
> 2) The spec can be "executed" (i.e., there is an
>>  interpreting mechanism, which lets the spec behave
>>  like the real thing).
>
> Not always reasonable.
>
> First, it is often the case that a spec does not describe execution at
> all. See, for example, the specification of a sorting function I give
> at the end of this message: it simply says "a sorting function is a
> function such that, for all inputs, the return is a non-decreasing
> permutation of the input". This is not executable. It is a purely
> descriptive property, and you cannot extract an executable algorithm
> from the spec.
>
> Second, even when a spec amounts to a description of execution, a
> proof assistant often cannot actually execute it. For example,
> although you can reason about non-terminating execution in pCiC (and
> thus Coq), programs written in a strongly normalizing lambda calculus
> that can be used as a logic must terminate, or functions that did not
> terminate would be inhabitants of all types and the logic would be
> inconsistent. Thus, you cannot execute a program with infinite loops
> inside Coq, although you can reason about them (and indeed, you can
> reason about coinductively defined objects like infinite execution
> traces.)
>
> On Mon, 06 Aug 2018 14:19:31 -0700 "Steve Johnson" <scj@yaccman.com>
> wrote:
>> I take a somewhat more relaxed view of what a spec should be:
>> It should describe a program with enough completeness that a
>> competent programmer could write it from the spec alone.
>
> I think this is a bit more relaxed than is currently accepted.
>
>> The formal systems I have seen would roll over and die when
>> presented with even a simple compiler.__
>
> I don't know what this means. If it is that there aren't
> implementations of languages like pCiC, that's not true, see Coq. If
> it means no one can formally specify a compiler, given that formally
> verified compilers exist, that's also not true.
>
> The "final theorem" proving the correctness of CompCert depends on
> having an operational semantics of both C and the target architecture,
> and says (more or less) that the observed behavior of the input
> program in C is the same as the observed behavior of the output
> program (say in ARM machine language). This is a serious piece of
> work, but it is also something that has actually been done -- the
> tools are capable of the task.
>
>> Additionally, being able to specify that a particular function be
>> carried out by a heapsort, for example, would require that the
>> formalism could describe the heapsort and prove it correct.__ These
>> don't grow on trees...
>
> Formally verifying a couple of sorting algorithms described in Coq is
> a exercise for an intro level class on formal verification. I've done
> it. Once you have the proper primitives described, the specification
> for a sorting algorithm in Coq looks like this:
>
> Definition is_a_sorting_algorithm (f: list nat -> list nat) :=
>   forall al, Permutation al (f al) /\ sorted (f al).
>
> That says "the property "is_a_sorting_algorithm" over a function from
> lists of natural numbers to lists of natural numbers is that the
> output is a permutation of the input in which all the elements are in
> non-decreasing order." The definitions in question are very
> precise. For example, one definition of sorted (the property of being
> a non-decreasing list) is:
>
> Definition sorted (al: list nat) :=
>  forall i j, i < j < length al -> nth i al 0 <= nth j al 0.
>
> and the property of being a permutation, which is relatively
> complicated inductively defined property, is:
>
> Inductive Permutation {A : Type} : list A -> list A -> Prop :=
>     perm_nil : Permutation
>   | perm_skip : forall (x : A) (l l' : list A),
>                 Permutation l l' ->
>                 Permutation (x :: l) (x :: l')
>   | perm_swap : forall (x y : A) (l : list A),
>                 Permutation (y :: x :: l) (x :: y :: l)
>   | perm_trans : forall l l' l'' : list A,
>                  Permutation l l' ->
>                  Permutation l' l'' ->
>                  Permutation l l''.
>
> Coq starts out with basically nothing defined, by the way. Notions
> such as "natural number" and "list" are not built in. Peano naturals
> are defined in the system thusly:
>
> Inductive nat : Type :=
>   | O : nat
>   | S : nat -> nat.
>
> The underlying basis of Coq (i.e. the Predicative Calculus of
> Inductive Constructions) is a dependently typed lambda calculus that's
> astonishingly simple, and the checker for proofs in the system is only
> a few hundred lines long -- the checker is the only portion of the
> system which needs to be trusted.
>
> In recent years, I've noted that "old timers" (such as many of us,
> myself included) seem to be unaware of the fact that systems like Coq
> exist, or that it is now relatively (I emphasize _relatively_) routine
> for substantial systems to be fully formally specified and then fully
> formally verified.
>
>
> Perry
> --
> Perry E. Metzger                perry@piermont.com

Re: [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[Perry E. Metzger]

On Mon, 20 Aug 2018 09:47:58 +1000 George Michaelson
<ggm@algebras.org> wrote:
> Witness to this, the interest in *trying* to apply Coq to Ethereum
> smart contracts...

The Tezos cryptocurrency was created with a smart contract language
specifically designed for formal verification.

> I think Perry wrote something of long term value. I encourage you to
> write this up somewhere you'd be willing to have published like a
> tech blog.

Not sure where one would publish it.

I also note that the general response here was the one I almost always
get when I mention this stuff to people, which is near silence. (I
used to get exactly this response 30 or 35 years ago when explaining
the Internet to most people who had not yet come into contact with it,
so I suppose it's not overly surprising.)

That said, let me make a strong prediction: in not very many years,
pretty much everyone doing serious work in computer science (say,
designing security protocols, building mission critical systems, etc.)
will be building them using some sort of formal verification assistant
systems. I suspect this change will be as transformative as the
triumph of high level languages over the previous supremacy of machine
language coding. (For those that forget, one of the things that made
Unix successful was, of course, that unlike many other OSes of the
era, it was (ultimately) written in a portable language and not in
machine code.)

People who don't use formal verification when writing serious code
will seem as antiquated and irresponsible as people who build mission
critical systems now without test coverage. This is going to be a big
revolution.


Perry


> -G
> 
> On Sun, Aug 19, 2018 at 5:57 AM, Perry E. Metzger
> <perry@piermont.com> wrote:
> > Sorry for the thread necromancy, but this is a _very_ important
> > topic. Perhaps it doesn't belong on tuhs but rather on coff.
> >
> > This is a pretty long posting. If you don't care to read it, the
> > TL;DR is that formal specification and verification is now a real
> > discipline, which it wasn't in the old days, and there are
> > systems to do it in, and it's well understood.
> >
> > On 2018-08-06 at 08:52 -0700, Bakul Shah wrote:  
> >>
> >> What counts as a "formal spec"? Is it like Justice Potter
> >> Stewart's "I know it when I see it" definition or something
> >> better?  
> >
> > At this point, we have a good definition. A formal specification
> > is a description of the behavior of a program or piece of
> > hardware in a precise machine-readable form that may be used as
> > the basis for fully formal verification of the behavior of an
> > implementation. Often these days, the specification is given in a
> > formal logic, such as the predicative calculus of inductive
> > constructions, which is the logic underlying the Coq system.
> >
> > Isabelle/HOL is another popular system for this sort of work.
> > ACL2 is (from what I can tell) of more historical interest but it
> > has apparently been used for things like the formal verification
> > of floating point and cache control units for real hardware. (It
> > is my understanding that it has been many years since Intel would
> > dare release a system where the cache unit wasn't verified, and
> > the only time in decades it tried to release a non-verified FPU,
> > it got the FDIV bug and has never tried that again.) There are
> > some others out there, like F*, Lean, etc.
> >
> > Formal specifications good enough for full formal verification
> > have been made for a variety of artifacts along with proofs that
> > the artifacts follow the specification. There's a fully formally
> > verified C compiler called CompCert for example, based on an
> > operational semantics written in Coq. There's another formal
> > semantics for C written in K, which is a rather different formal
> > system. There's a verified microkernel, seL4, whose specification
> > is written in Isabelle/HOL. There's a fully formal specification
> > of the RISC V, and an associated verified RTL implementation.
> >
> > Generally speaking, a formal specification:
> >
> > 1) Must be machine readable
> > 2) The semantics of the underlying specification language must
> >    themselves be extremely precisely described. You can't prove
> > the consistency and completeness of the underlying system (see
> > G__del) but you _can_ still strongly specify the language.
> > 3) Must be usable for formal (that is, machine checkable) proofs
> > that implementations comply with the spec, so it has to be
> > sufficiently powerful. Typical systems are now equivalent to
> > higher order logic.
> >
> > From: "Hellwig Geisse" <hellwig.geisse@mni.thm.de>
> > Sent:Mon, 06 Aug 2018 18:30:30 +0200  
> >>
> >>  For me, a "formal spec" should serve two goals:
> >>  1) You can reason about the thing that is specified.  
> >
> > Yes.
> >
> > 2) The spec can be "executed" (i.e., there is an  
> >>  interpreting mechanism, which lets the spec behave
> >>  like the real thing).  
> >
> > Not always reasonable.
> >
> > First, it is often the case that a spec does not describe
> > execution at all. See, for example, the specification of a
> > sorting function I give at the end of this message: it simply
> > says "a sorting function is a function such that, for all inputs,
> > the return is a non-decreasing permutation of the input". This is
> > not executable. It is a purely descriptive property, and you
> > cannot extract an executable algorithm from the spec.
> >
> > Second, even when a spec amounts to a description of execution, a
> > proof assistant often cannot actually execute it. For example,
> > although you can reason about non-terminating execution in pCiC
> > (and thus Coq), programs written in a strongly normalizing lambda
> > calculus that can be used as a logic must terminate, or functions
> > that did not terminate would be inhabitants of all types and the
> > logic would be inconsistent. Thus, you cannot execute a program
> > with infinite loops inside Coq, although you can reason about
> > them (and indeed, you can reason about coinductively defined
> > objects like infinite execution traces.)
> >
> > On Mon, 06 Aug 2018 14:19:31 -0700 "Steve Johnson"
> > <scj@yaccman.com> wrote:  
> >> I take a somewhat more relaxed view of what a spec should be:
> >> It should describe a program with enough completeness that a
> >> competent programmer could write it from the spec alone.  
> >
> > I think this is a bit more relaxed than is currently accepted.
> >  
> >> The formal systems I have seen would roll over and die when
> >> presented with even a simple compiler.__  
> >
> > I don't know what this means. If it is that there aren't
> > implementations of languages like pCiC, that's not true, see Coq.
> > If it means no one can formally specify a compiler, given that
> > formally verified compilers exist, that's also not true.
> >
> > The "final theorem" proving the correctness of CompCert depends on
> > having an operational semantics of both C and the target
> > architecture, and says (more or less) that the observed behavior
> > of the input program in C is the same as the observed behavior of
> > the output program (say in ARM machine language). This is a
> > serious piece of work, but it is also something that has actually
> > been done -- the tools are capable of the task.
> >  
> >> Additionally, being able to specify that a particular function be
> >> carried out by a heapsort, for example, would require that the
> >> formalism could describe the heapsort and prove it correct.__
> >> These don't grow on trees...  
> >
> > Formally verifying a couple of sorting algorithms described in
> > Coq is a exercise for an intro level class on formal
> > verification. I've done it. Once you have the proper primitives
> > described, the specification for a sorting algorithm in Coq looks
> > like this:
> >
> > Definition is_a_sorting_algorithm (f: list nat -> list nat) :=
> >   forall al, Permutation al (f al) /\ sorted (f al).
> >
> > That says "the property "is_a_sorting_algorithm" over a function
> > from lists of natural numbers to lists of natural numbers is that
> > the output is a permutation of the input in which all the
> > elements are in non-decreasing order." The definitions in
> > question are very precise. For example, one definition of sorted
> > (the property of being a non-decreasing list) is:
> >
> > Definition sorted (al: list nat) :=
> >  forall i j, i < j < length al -> nth i al 0 <= nth j al 0.
> >
> > and the property of being a permutation, which is relatively
> > complicated inductively defined property, is:
> >
> > Inductive Permutation {A : Type} : list A -> list A -> Prop :=
> >     perm_nil : Permutation
> >   | perm_skip : forall (x : A) (l l' : list A),
> >                 Permutation l l' ->
> >                 Permutation (x :: l) (x :: l')
> >   | perm_swap : forall (x y : A) (l : list A),
> >                 Permutation (y :: x :: l) (x :: y :: l)
> >   | perm_trans : forall l l' l'' : list A,
> >                  Permutation l l' ->
> >                  Permutation l' l'' ->
> >                  Permutation l l''.
> >
> > Coq starts out with basically nothing defined, by the way. Notions
> > such as "natural number" and "list" are not built in. Peano
> > naturals are defined in the system thusly:
> >
> > Inductive nat : Type :=
> >   | O : nat
> >   | S : nat -> nat.
> >
> > The underlying basis of Coq (i.e. the Predicative Calculus of
> > Inductive Constructions) is a dependently typed lambda calculus
> > that's astonishingly simple, and the checker for proofs in the
> > system is only a few hundred lines long -- the checker is the
> > only portion of the system which needs to be trusted.
> >
> > In recent years, I've noted that "old timers" (such as many of us,
> > myself included) seem to be unaware of the fact that systems like
> > Coq exist, or that it is now relatively (I emphasize
> > _relatively_) routine for substantial systems to be fully
> > formally specified and then fully formally verified.
> >
> >
> > Perry
> > --
> > Perry E. Metzger                perry@piermont.com  
> 



-- 
Perry E. Metzger		perry@piermont.com

Re: [TUHS] Formal Specification and Verification

[Warren Toomey]

I've forwarded the last e-mail in this thread to the COFF mailing list,
as it's strictly not TUHS related. Feel free to continue engaging in the
conversation over there!

Cheers, Warren

Re: [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[Tony Finch]

Perry E. Metzger <perry@piermont.com> wrote:
>
> This is a pretty long posting. If you don't care to read it, the TL;DR
> is that formal specification and verification is now a real
> discipline, which it wasn't in the old days, and there are systems to
> do it in, and it's well understood.

Another example, of a somewhat different flavour, is
http://lamport.azurewebsites.net/tla/amazon.html

The difference being that I gather Amazon are using TLA+ more as a
modelling language for distributed systems and not strictly for verifying
implementations.

PS. If there is a historical Lamport / Unix connection, I'm not aware of
one...

Tony.
-- 
f.anthony.n.finch  <dot@dotat.at>  http://dotat.at/
protect and enlarge the conditions of liberty and social justice

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Noel Chiappa]

    > I'm not into that stuff, so I point you in the right direction.
                                   ^
Sorry, lost a "can't" there.

       Noel

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Noel Chiappa]

    > From: Bakul Shah

    > What counts as a "formal spec"?

If you aren't familiar with the work in the field (it's been going on long
enough, it was around when I was an undergrad), some of the earlier messages
in the thread, e.g.:

  https://minnie.tuhs.org//pipermail/tuhs/2018-August/014365.html

might provide some thing you could follow. (I'm not into that stuff, so I
point you in the right direction.)

      Noel

Re: [TUHS] TUHS Digest, Vol 33, Issue 5

[Steve Simon]

well spec’ed machines where more common in the past. we had all the source for the interdata 3210 at college.

we had the edition 7 source, the driver source, the diagnostic tape source, and even  all the schematics.

two of the lecturers even upgraded it from 1mb to 4mb of RAM, complete with address decoders on their backs with their legs in the air.

-Steve

> On 6 Aug 2018, at 03:00, tuhs-request@minnie.tuhs.org wrote:
> 
> Send TUHS mailing list submissions to
>    tuhs@minnie.tuhs.org
> 
> To subscribe or unsubscribe via the World Wide Web, visit
>    https://minnie.tuhs.org/cgi-bin/mailman/listinfo/tuhs
> or, via email, send a message with subject or body 'help' to
>    tuhs-request@minnie.tuhs.org
> 
> You can reach the person managing the list at
>    tuhs-owner@minnie.tuhs.org
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of TUHS digest..."
> 
> 
> Today's Topics:
> 
>   1. Re: In Memoriam: Per Brinch Hansen (Perry E. Metzger)
>   2. Latest Kernighan interview on Youtube (Warren Toomey)
>   3. In Memoriam: Edsger Dijkstra, and happy birthday Jon Postel!
>      (Dave Horsfall)
>   4. Re: In Memoriam: Edsger Dijkstra,    and happy birthday Jon
>      Postel! (Noel Chiappa)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Sun, 5 Aug 2018 19:18:18 -0400
> From: "Perry E. Metzger" <perry@piermont.com>
> To: Doug McIlroy <doug@cs.dartmouth.edu>
> Cc: tuhs@tuhs.org
> Subject: Re: [TUHS] In Memoriam: Per Brinch Hansen
> Message-ID: <20180805191818.0ac05b0f@jabberwock.cb.piermont.com>
> Content-Type: text/plain; charset=US-ASCII
> 
> On Thu, 02 Aug 2018 08:44:56 -0400 Doug McIlroy
> <doug@cs.dartmouth.edu> wrote:
>> A tangential connection to early Unix experience:
>> 
>> My collection of early computer manuals includes Brinch Hansen's
>> manual for the RC 4000, which stands out for its precise
>> description of the CPU logic--in Algol 60! It's the only manual I
>> have seen that offers a good-to-the-last-bit formal description of
>> the hardware.
>> 
>> DEC presented something of the sort for the PDP-11, but punted where
>> the woods got thick. When I wanted to know how they computed the
>> last bit of floating-point results, I got no satisfaction. Amidst a
>> thorough description of addressing came this formulation of the
>> actual computation: "form floating point result".
> 
> For those that are familiar with the RISC V architecture, there's a
> formal specification of the architecture that was done in a system
> built on Coq, and also a fully formally verified translation of the
> specification into RTL. (The spec didn't include floating point as of
> about a year ago but it may by now.)
> 
> A good overview of the system involved is here:
> 
> http://plv.csail.mit.edu/kami/papers/icfp17.pdf
> 
> Followups might belong on the coff list, not sure.
> 
> Perry
> -- 
> Perry E. Metzger        perry@piermont.com
> 
> 
> ------------------------------
> 
> Message: 2
> Date: Mon, 6 Aug 2018 09:53:19 +1000
> From: Warren Toomey <wkt@tuhs.org>
> To: tuhs@tuhs.org
> Subject: [TUHS] Latest Kernighan interview on Youtube
> Message-ID: <20180805235319.GA14811@minnie.tuhs.org>
> Content-Type: text/plain; charset=us-ascii
> 
> in 3 parts:
> 
> https://www.youtube.com/watch?v=zmYhR8cUX90
> https://www.youtube.com/watch?v=VVpRj3Po6K4
> https://www.youtube.com/watch?v=E6vtRm5M8I0
> 
> Cheers, Warren
> 
> 
> ------------------------------
> 
> Message: 3
> Date: Mon, 6 Aug 2018 10:04:17 +1000 (EST)
> From: Dave Horsfall <dave@horsfall.org>
> To: The Eunuchs Hysterical Society <tuhs@tuhs.org>
> Subject: [TUHS] In Memoriam: Edsger Dijkstra, and happy birthday Jon
>    Postel!
> Message-ID:
>    <alpine.BSF.2.21.9999.1808060955320.79568@aneurin.horsfall.org>
> Content-Type: text/plain; charset=US-ASCII; format=flowed
> 
> What a weird day...
> 
> We lost computer pioneer Edsger Dijkstra in 2002; he gave us ALGOL, 
> structured programming, semaphores, and ranted against the GOTO statement 
> (much to the distress of the Fortranites and their spaghetti coding). 
> Oh, and a certain Prof. Goto used to complain that everybody wanted to 
> eliminate him :-)
> 
> However, we gained Jon Postel in 1943; with umpteen RFCs to his name, he 
> could pretty much be described as the Father of the Internet.
> 
> -- 
> Dave Horsfall DTM (VK2KFU)  "Those who don't understand security will suffer."
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Sun,  5 Aug 2018 21:15:45 -0400 (EDT)
> From: jnc@mercury.lcs.mit.edu (Noel Chiappa)
> To: tuhs@tuhs.org
> Cc: jnc@mercury.lcs.mit.edu
> Subject: Re: [TUHS] In Memoriam: Edsger Dijkstra,    and happy birthday
>    Jon Postel!
> Message-ID: <20180806011545.29C1F18C09A@mercury.lcs.mit.edu>
> 
>> From: Dave Horsfall
> 
>> However, we gained Jon Postel in 1943; with umpteen RFCs to his name, he
>> could pretty much be described as the Father of the Internet.
> 
> The problem with using the number of documents as a gauge for that is that Jon
> often acted as scribe, so that for many things published under his name, he
> was acting more as editor.
> 
> As to who (if anyone) does deserve that title, I'm also not sure about the
> importance of Cerf and Kahn. NOTE: I am not saying they _didn't_ make the key
> contribution - I just haven't looked into it in enough detail to say.
> 
> For example, before the TCP/IP effort got rolling, there was something called
> the International Packet Network Working Group (INWG) which had a big role,
> but which has been poorly documented. There's a note called "The Internet: On
> its International Origins and Collaborative Vision" by Rhonda Hauben,
> available here:
> 
>  http://www.columbia.edu/~rh120/other/misc/haubenpap.rtf
> 
> which covers it some, and there's a more recent thing by Alex Mackenzie which
> is probably better, but I'm too lazy to go find it.
> 
> Louis Pouzin (or whoever it was at CYCLADES who actually had the idea to move
> the reliability out of the packet switches, and into the hosts), also would
> have a good claim to the title.
> 
> 
> Anyway, sorry for the offtopic, but my 'fake history' alarm went off...
> 
>    Noel
> 
> 
> ------------------------------
> 
> Subject: Digest Footer
> 
> _______________________________________________
> TUHS mailing list
> TUHS@minnie.tuhs.org
> https://minnie.tuhs.org/cgi-bin/mailman/listinfo/tuhs
> 
> ------------------------------
> 
> End of TUHS Digest, Vol 33, Issue 5
> ***********************************