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

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

[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 --]

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

[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

[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

[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

[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
> ***********************************