Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Profanity is the one language all programmers know best.


devel / comp.arch.embedded / Re: (Semi-) formal methods

SubjectAuthor
* (Semi-) formal methodsDon Y
+* Re: (Semi-) formal methodsTheo
|`* Re: (Semi-) formal methodsDon Y
| `* Re: (Semi-) formal methodsTheo
|  `* Re: (Semi-) formal methodsDon Y
|   +* Re: (Semi-) formal methodsHT-Lab
|   |`- Re: (Semi-) formal methodsDon Y
|   `* Re: (Semi-) formal methodsTheo
|    `- Re: (Semi-) formal methodsDon Y
+* Re: (Semi-) formal methodsDave Nadler
|+- Re: (Semi-) formal methodsDon Y
|`- Re: (Semi-) formal methodsPaul Rubin
`* Re: (Semi-) formal methodsClifford Heath
 `* Re: (Semi-) formal methodsDon Y
  +- Re: (Semi-) formal methodsDon Y
  `* Re: (Semi-) formal methodsClifford Heath
   `* Re: (Semi-) formal methodsDon Y
    `* Re: (Semi-) formal methodsClifford Heath
     `* Re: (Semi-) formal methodsDon Y
      `* Re: (Semi-) formal methodsClifford Heath
       `* Re: (Semi-) formal methodsDon Y
        `* Re: (Semi-) formal methodsClifford Heath
         `* Re: (Semi-) formal methodsDon Y
          `* Re: (Semi-) formal methodsClifford Heath
           `* Re: (Semi-) formal methodsDon Y
            `* Re: (Semi-) formal methodsClifford Heath
             `- Re: (Semi-) formal methodsDon Y

Pages:12
(Semi-) formal methods

<s7fara$f23$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=430&group=comp.arch.embedded#430

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: (Semi-) formal methods
Date: Tue, 11 May 2021 18:25:57 -0700
Organization: A noiseless patient Spider
Lines: 4
Message-ID: <s7fara$f23$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 12 May 2021 01:26:02 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="55b1970268c00f05e77349fdb3a20754";
logging-data="15427"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+gNwjJRqRdRSiKcF2vDaIs"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:TXIq/+LWsnId0NvdpwhNtLq9QqU=
Content-Language: en-US
X-Mozilla-News-Host: news://news.eternal-september.org:119
 by: Don Y - Wed, 12 May 2021 01:25 UTC

How prevalent are (semi-) formal design methods employed?
Which?

[I don't have first-hand knowledge of *anyone* using them]

Re: (Semi-) formal methods

<yqf*720jy@news.chiark.greenend.org.uk>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=434&group=comp.arch.embedded#434

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!aioe.org!nntp.terraraq.uk!nntp-feed.chiark.greenend.org.uk!ewrotcd!.POSTED!not-for-mail
From: theom+n...@chiark.greenend.org.uk (Theo)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: 13 May 2021 15:25:48 +0100 (BST)
Organization: University of Cambridge, England
Lines: 10
Message-ID: <yqf*720jy@news.chiark.greenend.org.uk>
References: <s7fara$f23$1@dont-email.me>
NNTP-Posting-Host: chiark.greenend.org.uk
X-Trace: chiark.greenend.org.uk 1620915950 26391 212.13.197.229 (13 May 2021 14:25:50 GMT)
X-Complaints-To: abuse@chiark.greenend.org.uk
NNTP-Posting-Date: Thu, 13 May 2021 14:25:50 +0000 (UTC)
User-Agent: tin/1.8.3-20070201 ("Scotasay") (UNIX) (Linux/3.16.0-7-amd64 (x86_64))
Originator: theom@chiark.greenend.org.uk ([212.13.197.229])
 by: Theo - Thu, 13 May 2021 14:25 UTC

Don Y <blockedofcourse@foo.invalid> wrote:
> How prevalent are (semi-) formal design methods employed?
> Which?

We use theorem provers to find bugs in ISA specification:
https://www.cl.cam.ac.uk/~pes20/sail/

They're quite handy for finding bugs before they hit silicon...

Theo

Re: (Semi-) formal methods

<s7jsr8$77r$3@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=437&group=comp.arch.embedded#437

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Thu, 13 May 2021 11:57:36 -0700
Organization: A noiseless patient Spider
Lines: 15
Message-ID: <s7jsr8$77r$3@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<yqf*720jy@news.chiark.greenend.org.uk>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 13 May 2021 18:57:44 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="e89e6803c8ce1200046fd32bd46abad8";
logging-data="7419"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18t537Aqk2VOggRexLxE2pC"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:C+K4h2InFwksVfsJikA0DCk0+G0=
In-Reply-To: <yqf*720jy@news.chiark.greenend.org.uk>
Content-Language: en-US
 by: Don Y - Thu, 13 May 2021 18:57 UTC

On 5/13/2021 7:25 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote:
>> How prevalent are (semi-) formal design methods employed?
>> Which?
>
> We use theorem provers to find bugs in ISA specification:
> https://www.cl.cam.ac.uk/~pes20/sail/
>
> They're quite handy for finding bugs before they hit silicon...

But, presumably, only of value if you're a SoC integrator?

I.e., given COTS devices, what might they reveal to users of
said devices?

Re: (Semi-) formal methods

<s7kcug$1usj$1@gioia.aioe.org>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=440&group=comp.arch.embedded#440

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!aioe.org!Tgip5Y7XolJj69PZynN/8Q.user.gioia.aioe.org.POSTED!not-for-mail
From: drn...@nadler.com (Dave Nadler)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Thu, 13 May 2021 19:32:33 -0400
Organization: Aioe.org NNTP Server
Lines: 4
Message-ID: <s7kcug$1usj$1@gioia.aioe.org>
References: <s7fara$f23$1@dont-email.me>
NNTP-Posting-Host: Tgip5Y7XolJj69PZynN/8Q.user.gioia.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.10.1
Content-Language: en-US
X-Notice: Filtered by postfilter v. 0.9.2
 by: Dave Nadler - Thu, 13 May 2021 23:32 UTC

On 5/11/2021 9:25 PM, Don Y wrote:
> How prevalent are (semi-) formal design methods employed?

https://tinyurl.com/thbjw5j4

Re: (Semi-) formal methods

<s7keeb$vpg$2@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=442&group=comp.arch.embedded#442

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Thu, 13 May 2021 16:57:55 -0700
Organization: A noiseless patient Spider
Lines: 7
Message-ID: <s7keeb$vpg$2@dont-email.me>
References: <s7fara$f23$1@dont-email.me> <s7kcug$1usj$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 13 May 2021 23:58:04 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d202010a663ab97d7afd0c23f0dad6da";
logging-data="32560"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18B6Gw0hTaoXIVu6TIjI0D/"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:zLBEXXSDKFxUUv7Nh9M57QKieOM=
In-Reply-To: <s7kcug$1usj$1@gioia.aioe.org>
Content-Language: en-US
 by: Don Y - Thu, 13 May 2021 23:57 UTC

On 5/13/2021 4:32 PM, Dave Nadler wrote:
> On 5/11/2021 9:25 PM, Don Y wrote:
>> How prevalent are (semi-) formal design methods employed?
>
> https://tinyurl.com/thbjw5j4

Hardly formal -- no cufflinks, watchfob, cumberbund nor tails! :>

Re: (Semi-) formal methods

<Bqf*jg5jy@news.chiark.greenend.org.uk>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=443&group=comp.arch.embedded#443

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!aioe.org!nntp.terraraq.uk!nntp-feed.chiark.greenend.org.uk!ewrotcd!.POSTED!not-for-mail
From: theom+n...@chiark.greenend.org.uk (Theo)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: 14 May 2021 10:43:03 +0100 (BST)
Organization: University of Cambridge, England
Lines: 23
Message-ID: <Bqf*jg5jy@news.chiark.greenend.org.uk>
References: <s7fara$f23$1@dont-email.me> <yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me>
NNTP-Posting-Host: chiark.greenend.org.uk
X-Trace: chiark.greenend.org.uk 1620985385 7891 212.13.197.229 (14 May 2021 09:43:05 GMT)
X-Complaints-To: abuse@chiark.greenend.org.uk
NNTP-Posting-Date: Fri, 14 May 2021 09:43:05 +0000 (UTC)
User-Agent: tin/1.8.3-20070201 ("Scotasay") (UNIX) (Linux/3.16.0-7-amd64 (x86_64))
Originator: theom@chiark.greenend.org.uk ([212.13.197.229])
 by: Theo - Fri, 14 May 2021 09:43 UTC

Don Y <blockedofcourse@foo.invalid> wrote:
> On 5/13/2021 7:25 AM, Theo wrote:
> > Don Y <blockedofcourse@foo.invalid> wrote:
> >> How prevalent are (semi-) formal design methods employed?
> >> Which?
> >
> > We use theorem provers to find bugs in ISA specification:
> > https://www.cl.cam.ac.uk/~pes20/sail/
> >
> > They're quite handy for finding bugs before they hit silicon...
>
> But, presumably, only of value if you're a SoC integrator?
>
> I.e., given COTS devices, what might they reveal to users of
> said devices?

They can reveal bugs in existing implementations - where they don't meet the
spec and bad behaviour can result.

However CPU and FPGA design is what we do so that's where we focus our
efforts. Depends whether FPGA counts as COTS or not...

Theo

Re: (Semi-) formal methods

<87bl9dyvbc.fsf@nightsong.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=446&group=comp.arch.embedded#446

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: no.em...@nospam.invalid (Paul Rubin)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Fri, 14 May 2021 12:22:31 -0700
Organization: A noiseless patient Spider
Lines: 9
Message-ID: <87bl9dyvbc.fsf@nightsong.com>
References: <s7fara$f23$1@dont-email.me> <s7kcug$1usj$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="8b9c7676d27c13b7027087884137afe1";
logging-data="24467"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+93C0q0LFQMChLZF7jQxP9"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:Wu4AMjXK9fiJx4ozvkHexx9XSVo=
sha1:C6UC1nf/N43Cndq+LHtCoh6XPK4=
 by: Paul Rubin - Fri, 14 May 2021 19:22 UTC

Dave Nadler <drn@nadler.com> writes:
>> How prevalent are (semi-) formal design methods employed?
> https://tinyurl.com/thbjw5j4

Wrong picture, try the one on this page:

https://web.stanford.edu/~engler/

Look at the articles linked from there too ;-).

Re: (Semi-) formal methods

<s7mjh8$vcj$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=447&group=comp.arch.embedded#447

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Fri, 14 May 2021 12:37:09 -0700
Organization: A noiseless patient Spider
Lines: 31
Message-ID: <s7mjh8$vcj$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me>
<Bqf*jg5jy@news.chiark.greenend.org.uk>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Fri, 14 May 2021 19:37:13 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d202010a663ab97d7afd0c23f0dad6da";
logging-data="32147"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX185JtNz4s8OfQ0+6Z1c7D1D"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:tbUNem85q5yzhvUrSx2c4nUwJ3E=
In-Reply-To: <Bqf*jg5jy@news.chiark.greenend.org.uk>
Content-Language: en-US
 by: Don Y - Fri, 14 May 2021 19:37 UTC

On 5/14/2021 2:43 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote:
>> On 5/13/2021 7:25 AM, Theo wrote:
>>> Don Y <blockedofcourse@foo.invalid> wrote:
>>>> How prevalent are (semi-) formal design methods employed?
>>>> Which?
>>>
>>> We use theorem provers to find bugs in ISA specification:
>>> https://www.cl.cam.ac.uk/~pes20/sail/
>>>
>>> They're quite handy for finding bugs before they hit silicon...
>>
>> But, presumably, only of value if you're a SoC integrator?
>>
>> I.e., given COTS devices, what might they reveal to users of
>> said devices?
>
> They can reveal bugs in existing implementations - where they don't meet the
> spec and bad behaviour can result.
>
> However CPU and FPGA design is what we do so that's where we focus our
> efforts. Depends whether FPGA counts as COTS or not...

Understood. Tools fit the application domains for which they were designed.

How did *adoption* of the tool come to pass? Was it "mandated" by corporate
policy? Something <someone> stumbled on, played with and then "pitched"
to management/peers? Mandated by your industry? etc.

[Just because a tool "makes sense" -- logically or economically -- doesn't
mean it will be adopted, much less *embraced*!]

Re: (Semi-) formal methods

<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=448&group=comp.arch.embedded#448

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Sat, 15 May 2021 14:15:15 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s7fara$f23$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
Lines: 16
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!feeder1.feed.usenet.farm!feed.usenet.farm!news-out.netnews.com!news.alt.net!fdc3.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::41.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Sat, 15 May 2021 04:15:15 +0000
X-Complaints-To: abuse@thecubenet.com
Organization: theCubeNet - www.thecubenet.com
X-Received-Bytes: 1534
 by: Clifford Heath - Sat, 15 May 2021 04:15 UTC

On 12/5/21 11:25 am, Don Y wrote:
> How prevalent are (semi-) formal design methods employed?
> Which?
>
> [I don't have first-hand knowledge of *anyone* using them]

Don, IDK if you know about TLA+, but there is a growing community using
it. It is specifically good at finding errors in protocol (== API)
designs (because "TL" means "Temporal Logic"). I haven't used it so
can't really answer many questions, but I have been following the
mailing list for some time and greatly admire some of the excellent folk
are are using it.

<https://learntla.com/introduction/>

Clifford Heath.

Re: (Semi-) formal methods

<s7nk3b$d0m$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=449&group=comp.arch.embedded#449

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Fri, 14 May 2021 21:52:47 -0700
Organization: A noiseless patient Spider
Lines: 36
Message-ID: <s7nk3b$d0m$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 04:52:59 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fbf32e3585750f687207bae26fde6b55";
logging-data="13334"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+5qKjZrW1pSwwt19NxUbml"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:dtW6+sIqMf4+qY9Jpkn1OxeKEYM=
In-Reply-To: <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 04:52 UTC

On 5/14/2021 9:15 PM, Clifford Heath wrote:
> On 12/5/21 11:25 am, Don Y wrote:
>> How prevalent are (semi-) formal design methods employed?
>> Which?
>>
>> [I don't have first-hand knowledge of *anyone* using them]
>
> Don, IDK if you know about TLA+, but there is a growing community using it. It
> is specifically good at finding errors in protocol (== API) designs (because
> "TL" means "Temporal Logic"). I haven't used it so can't really answer many
> questions, but I have been following the mailing list for some time and greatly
> admire some of the excellent folk are are using it.

My query was more intended to see how *commonplace* such approaches are.
There are (and have been) many "great ideas" but, from my vantage point,
I don't see much by way of *adoption*. (Note your own experience with TLA!)

[The "(Semi-)" was an accommodation for *individuals* who may be
using such things even though their work environment doesn't]

So, you either conclude that the methods are all "hype" (not likely),
*or*, there is some inherent resistance to their adoption. Price?
(Process) overhead? NIH? Scale? Education? <shrug>

[Note my followup question to Theo as to how *he/they* ended up with
their tool/process]

There seem to be many "lost opportunities" (?) for tools, techniques,
processes, etc. I'm just curious as to *why* (or, why *not*).
Or, said another way, what does a tool/process have to *do* in
order to overcome this "resistance"?

It's as if a (professional) writer wouldn't avail himself of a
spell-checker... Or, a layout guy not running DRCs... (yes,
I realize this to be an oversimplification; the examples I've
given are just mouse clicks!)

Re: (Semi-) formal methods

<s7nk7m$d0m$2@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=450&group=comp.arch.embedded#450

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Fri, 14 May 2021 21:55:15 -0700
Organization: A noiseless patient Spider
Lines: 10
Message-ID: <s7nk7m$d0m$2@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 04:55:18 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fbf32e3585750f687207bae26fde6b55";
logging-data="13334"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+X0SzeAA5iEcvrWyRrBeUZ"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:P2WDAyVt+MrJog/sHLSxmYFCBlU=
In-Reply-To: <s7nk3b$d0m$1@dont-email.me>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 04:55 UTC

On 5/14/2021 9:52 PM, Don Y wrote:
> Or, said another way, what does a tool/process have to *do* in
> order to overcome this "resistance"?

By "do", I mean in the colloquial sense, not a specific feature
set, etc.

I.e., "It has to make my dinner and wash the dishes in order
for me to consider it worth embracing" (or, "It has to cut
25% of the development cost from a project")

Re: (Semi-) formal methods

<6ZKnI.266611$F197.112760@fx07.ams4>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=451&group=comp.arch.embedded#451

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!newsfeed.xs4all.nl!newsfeed9.news.xs4all.nl!feeder1.feed.usenet.farm!feed.usenet.farm!peer01.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx07.ams4.POSTED!not-for-mail
Reply-To: hans64@htminuslab.com
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me>
<yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me>
<Bqf*jg5jy@news.chiark.greenend.org.uk> <s7mjh8$vcj$1@dont-email.me>
From: han...@htminuslab.com (HT-Lab)
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.10.1
MIME-Version: 1.0
In-Reply-To: <s7mjh8$vcj$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-GB
Content-Transfer-Encoding: 8bit
X-Antivirus: Avast (VPS 210515-0, 15/05/2021), Outbound message
X-Antivirus-Status: Clean
Lines: 53
Message-ID: <6ZKnI.266611$F197.112760@fx07.ams4>
X-Complaints-To: http://netreport.virginmedia.com
NNTP-Posting-Date: Sat, 15 May 2021 07:44:02 UTC
Organization: virginmedia.com
Date: Sat, 15 May 2021 08:44:01 +0100
X-Received-Bytes: 3095
 by: HT-Lab - Sat, 15 May 2021 07:44 UTC

On 14/05/2021 20:37, Don Y wrote:
> On 5/14/2021 2:43 AM, Theo wrote:
>> Don Y <blockedofcourse@foo.invalid> wrote:
>>> On 5/13/2021 7:25 AM, Theo wrote:
>>>> Don Y <blockedofcourse@foo.invalid> wrote:
>>>>> How prevalent are (semi-) formal design methods employed?
>>>>> Which?
>>>>
>>>> We use theorem provers to find bugs in ISA specification:
>>>> https://www.cl.cam.ac.uk/~pes20/sail/
>>>>
>>>> They're quite handy for finding bugs before they hit silicon...
>>>
>>> But, presumably, only of value if you're a SoC integrator?
>>>
>>> I.e., given COTS devices, what might they reveal to users of
>>> said devices?
>>
>> They can reveal bugs in existing implementations - where they don't
>> meet the
>> spec and bad behaviour can result.
>>
>> However CPU and FPGA design is what we do so that's where we focus our
>> efforts.  Depends whether FPGA counts as COTS or not...
>
> Understood.  Tools fit the application domains for which they were
> designed.
>
> How did *adoption* of the tool come to pass?  Was it "mandated" by
> corporate
> policy?  Something <someone> stumbled on, played with and then "pitched"
> to management/peers?  Mandated by your industry?  etc.
>

It became a must have tool about 2-3 decades ago for the safety
critical/ avionics/medical industries. Design where becoming so complex
that simulation could no longer answers questions like, is dead-lock or
life-lock possible on our statemachine, can you buffers overflow, do you
have arithmetic overflow, deadcode, race condition etc. The tools are
now well established and most of the above questions can be answered
(with some user constraints) by a simple push button tool. They are
still expensive (you won't get much change from 20K UK pounds) but most
high-end FPGA/ASIC companies use them. They are not a replacement for
simulation but one of the tools you need to complete your verification.

Regards,
Hans
www.ht-lab.com

> [Just because a tool "makes sense" -- logically or economically -- doesn't
> mean it will be adopted, much less *embraced*!]

Re: (Semi-) formal methods

<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=452&group=comp.arch.embedded#452

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me> <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com> <s7nk3b$d0m$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Sat, 15 May 2021 18:14:14 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s7nk3b$d0m$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
Lines: 51
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!feeder1.feed.usenet.farm!feed.usenet.farm!tr3.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::43.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Sat, 15 May 2021 08:14:16 +0000
X-Received-Bytes: 2967
Organization: theCubeNet - www.thecubenet.com
X-Complaints-To: abuse@thecubenet.com
 by: Clifford Heath - Sat, 15 May 2021 08:14 UTC

On 15/5/21 2:52 pm, Don Y wrote:
> On 5/14/2021 9:15 PM, Clifford Heath wrote:
>> On 12/5/21 11:25 am, Don Y wrote:
>>> How prevalent are (semi-) formal design methods employed?
>>> Which?
>>>
>>> [I don't have first-hand knowledge of *anyone* using them]
>>
>> Don, IDK if you know about TLA+, but there is a growing community
>> using it. It is specifically good at finding errors in protocol (==
>> API) designs (because "TL" means "Temporal Logic"). I haven't used it
>> so can't really answer many questions, but I have been following the
>> mailing list for some time and greatly admire some of the excellent
>> folk are are using it.
>
> My query was more intended to see how *commonplace* such approaches are.
> There are (and have been) many "great ideas" but, from my vantage point,
> I don't see much by way of *adoption*.  (Note your own experience with
> TLA!)

My own experience is irrelevant, as I was semi-retired when I first came
across it. On the other hand, the reason I came across it was I received
a message from Chris Newcombe (admiring my related work), whose success
in using it to find a potential failure in DynamoDB that could have
knocked *Amazon* off the air was a stimulus to many *many* folk learning
TLA+.

> So, you either conclude that the methods are all "hype" (not likely),
> *or*, there is some inherent resistance to their adoption.  Price?
> (Process) overhead?  NIH?  Scale?  Education?  <shrug>

For software folk at least, it requires a very different way of
thinking. The same problem I had promulgating fact-based modeling: both
address a massive *blind spot* in developer's consciousness.

Specifically we are unable to consciously detect when there is a failure
in our logic; because to be conscious of the failure it would have to be
*not present*. That is, we can only know such things in hindsight, or
when we deliberately apply specific methods to check our logic. But why
would we do that when it is "apparent" that our logic is correct?

> It's as if a (professional) writer wouldn't avail himself of a
> spell-checker...  Or, a layout guy not running DRCs...  (yes,
> I realize this to be an oversimplification; the examples I've
> given are just mouse clicks!)

These are not the same at all, because those things have rules. There is
no rule for correct logic.

Clifford Heath

Re: (Semi-) formal methods

<s7o35m$sfi$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=453&group=comp.arch.embedded#453

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Sat, 15 May 2021 02:10:01 -0700
Organization: A noiseless patient Spider
Lines: 40
Message-ID: <s7o35m$sfi$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 09:10:14 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fbf32e3585750f687207bae26fde6b55";
logging-data="29170"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19olZjVOGvqW0+MWlvDlrO5"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:dfczQ5uJFvxKvO1GvOFMJQdSudw=
In-Reply-To: <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 09:10 UTC

On 5/15/2021 1:14 AM, Clifford Heath wrote:

>> It's as if a (professional) writer wouldn't avail himself of a
>> spell-checker... Or, a layout guy not running DRCs... (yes,
>> I realize this to be an oversimplification; the examples I've
>> given are just mouse clicks!)
>
> These are not the same at all, because those things have rules. There is no
> rule for correct logic.

Logic is only "correct" if you are applying a prover.

You can still use formal methods in things like specifications -- where
there is no "proof" implied. The advantage being that everyone can
unambiguously understand the intent of the specification without lots
of (verbose) "legalese".

E.g., I did my initial design with OCL as the means by which I conveyed
my intent to my colleagues. It wasn't that much of a "lift" for them
to learn the representation well enough to ask pertinent questions and
"challenge" the implementation. And, didn't resort to lots of mathematical
abstraction to make those points.

Unfortunately, use in such a document is not suited for "general audiences"
because it lacks rationale for each item in the specification. (and,
relies on some semi-ubiquitous usage to ensure readers CAN read it)

OTOH, if you're writing the code (or reading it), such documents add
further texture to what you're seeing (in the programming language).
Another set of comments, so to speak. Or, a roadmap.

The alternative is: an /ad hoc/ specification (with some likely incompletely
specified set of loose rules) *or* an *absent* specification. Each of these
leave gaping holes in the design that (supposedly) follows.

Again, why the resistance to adopting such a "codified" approach?
There's no capital outlay required to adopt a *methodology* (unless
you want/need tools). It's as if the effort is seen as an *additional*
effort -- but with no perception of a "return". Is this because the
"return" doesn't stand out and have flashing lights surrounding it?

Re: (Semi-) formal methods

<s7o5dk$lev$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=454&group=comp.arch.embedded#454

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Sat, 15 May 2021 02:48:24 -0700
Organization: A noiseless patient Spider
Lines: 62
Message-ID: <s7o5dk$lev$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me>
<Bqf*jg5jy@news.chiark.greenend.org.uk> <s7mjh8$vcj$1@dont-email.me>
<6ZKnI.266611$F197.112760@fx07.ams4>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 09:48:37 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fbf32e3585750f687207bae26fde6b55";
logging-data="21983"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/D4T1fKm06WBZA8DGFF+mb"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:XFWNSB+5HSP14m1i/x8PhAXaTPg=
In-Reply-To: <6ZKnI.266611$F197.112760@fx07.ams4>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 09:48 UTC

On 5/15/2021 12:44 AM, HT-Lab wrote:
> On 14/05/2021 20:37, Don Y wrote:
>> On 5/14/2021 2:43 AM, Theo wrote:
>>> Don Y <blockedofcourse@foo.invalid> wrote:
>>>> On 5/13/2021 7:25 AM, Theo wrote:
>>>>> Don Y <blockedofcourse@foo.invalid> wrote:
>>>>>> How prevalent are (semi-) formal design methods employed?
>>>>>> Which?
>>>>>
>>>>> We use theorem provers to find bugs in ISA specification:
>>>>> https://www.cl.cam.ac.uk/~pes20/sail/
>>>>>
>>>>> They're quite handy for finding bugs before they hit silicon...
>>>>
>>>> But, presumably, only of value if you're a SoC integrator?
>>>>
>>>> I.e., given COTS devices, what might they reveal to users of
>>>> said devices?
>>>
>>> They can reveal bugs in existing implementations - where they don't meet the
>>> spec and bad behaviour can result.
>>>
>>> However CPU and FPGA design is what we do so that's where we focus our
>>> efforts. Depends whether FPGA counts as COTS or not...
>>
>> Understood. Tools fit the application domains for which they were designed.
>>
>> How did *adoption* of the tool come to pass? Was it "mandated" by corporate
>> policy? Something <someone> stumbled on, played with and then "pitched"
>> to management/peers? Mandated by your industry? etc.
>>
>
> It became a must have tool about 2-3 decades ago for the safety critical/
> avionics/medical industries.

But these are industries with inherently high levels of overhead -- possibly
suggesting (market) "efficiency" (in other industries) as a reason that
discourages adoption.

So, if it/they have value *there*, why aren't it/they embraced EVERYWHERE?
Obviously, other product offerings in other industries face similar design
problems...

> Design where becoming so complex that simulation
> could no longer answers questions like, is dead-lock or life-lock possible on
> our statemachine, can you buffers overflow, do you have arithmetic overflow,
> deadcode, race condition etc. The tools are now well established and most of
> the above questions can be answered (with some user constraints) by a simple
> push button tool. They are still expensive (you won't get much change from 20K
> UK pounds) but most high-end FPGA/ASIC companies use them. They are not a
> replacement for simulation but one of the tools you need to complete your
> verification.
>
> Regards,
> Hans
> www.ht-lab.com
>
>
>> [Just because a tool "makes sense" -- logically or economically -- doesn't
>> mean it will be adopted, much less *embraced*!]
>

Re: (Semi-) formal methods

<167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=455&group=comp.arch.embedded#455

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me> <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com> <s7nk3b$d0m$1@dont-email.me> <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com> <s7o35m$sfi$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Sat, 15 May 2021 20:54:10 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s7o35m$sfi$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
Lines: 57
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!3.eu.feeder.erje.net!feeder.erje.net!newsfeed.xs4all.nl!newsfeed9.news.xs4all.nl!tr3.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::44.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Sat, 15 May 2021 10:54:12 +0000
X-Received-Bytes: 3041
Organization: theCubeNet - www.thecubenet.com
X-Complaints-To: abuse@thecubenet.com
 by: Clifford Heath - Sat, 15 May 2021 10:54 UTC

On 15/5/21 7:10 pm, Don Y wrote:
> On 5/15/2021 1:14 AM, Clifford Heath wrote:
>
>>> It's as if a (professional) writer wouldn't avail himself of a
>>> spell-checker...  Or, a layout guy not running DRCs...  (yes,
>>> I realize this to be an oversimplification; the examples I've
>>> given are just mouse clicks!)
>>
>> These are not the same at all, because those things have rules. There
>> is no rule for correct logic.
>
> Logic is only "correct" if you are applying a prover.

I was loose with terminology. People tend to think that their
"reasoning" is correct and doesn't need to be logically analysed or
proved. They're wrong, but the blind spot is unavoidable.

Of course, there's also the problem that a thing may be "proved" yet be
(undetectably, until it becomes detectable) not what would have been
wanted - if it had been possible to foresee the failure mode.

> You can still use formal methods in things like specifications

That's how I used it, for static modelling (modelling all possible
"states of the world" as they may exist at a point in time). Although
dynamic modelling is much more exciting, it is rarely difficult once the
correct static model has been agreed.

<http://dataconstellation.com/ActiveFacts/CQLIntroduction.html>

> Unfortunately, use in such a document is not suited for "general audiences"

The goal of CQL is to make the formal model suitable for (and expressed
in the language of) anyone generally familiar with the domain being
modelled.

> because it lacks rationale for each item in the specification.

Actually rationale is seldom needed. What is needed is an example of the
scenario that is allowed or disallowed by each definition. The example
is almost always an adequate rationalisation.
> The alternative is: an /ad hoc/ specification (with some likely
> incompletely
> specified set of loose rules) *or* an *absent* specification.  Each of
> these leave gaping holes in the design that (supposedly) follows.

That's precisely true. That's why analytic (formal) models are needed.

> Again, why the resistance to adopting such a "codified" approach?

Hubris, mostly. People genuinely don't see the need until enough
experience has humbled them, and by then, their accumulated caution and
tentativeness mean their industry sees them as dinosaurs.

Clifford Heath.

Re: (Semi-) formal methods

<yqf*lQ+jy@news.chiark.greenend.org.uk>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=456&group=comp.arch.embedded#456

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!paganini.bofh.team!newsfeed.xs3.de!nntp-feed.chiark.greenend.org.uk!ewrotcd!.POSTED!not-for-mail
From: theom+n...@chiark.greenend.org.uk (Theo)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: 15 May 2021 12:02:04 +0100 (BST)
Organization: University of Cambridge, England
Lines: 34
Message-ID: <yqf*lQ+jy@news.chiark.greenend.org.uk>
References: <s7fara$f23$1@dont-email.me> <yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me> <Bqf*jg5jy@news.chiark.greenend.org.uk> <s7mjh8$vcj$1@dont-email.me>
NNTP-Posting-Host: chiark.greenend.org.uk
X-Trace: chiark.greenend.org.uk 1621076526 24213 212.13.197.229 (15 May 2021 11:02:06 GMT)
X-Complaints-To: abuse@chiark.greenend.org.uk
NNTP-Posting-Date: Sat, 15 May 2021 11:02:06 +0000 (UTC)
User-Agent: tin/1.8.3-20070201 ("Scotasay") (UNIX) (Linux/3.16.0-7-amd64 (x86_64))
Originator: theom@chiark.greenend.org.uk ([212.13.197.229])
 by: Theo - Sat, 15 May 2021 11:02 UTC

Don Y <blockedofcourse@foo.invalid> wrote:
> Understood. Tools fit the application domains for which they were designed.
>
> How did *adoption* of the tool come to pass? Was it "mandated" by corporate
> policy? Something <someone> stumbled on, played with and then "pitched"
> to management/peers? Mandated by your industry? etc.
>
> [Just because a tool "makes sense" -- logically or economically -- doesn't
> mean it will be adopted, much less *embraced*!]

We're a university research lab. We developed the tool in response to two
trends:

- growing complexity of systems and the increasing prevalence of bugs in
implementation (for example in memory coherency subsystems).

- proposing security extensions to architectures and wanting to be able to
show that what we've proposed doesn't have any loopholes in it. It provides
confidence to us and to people adopting the technology that the technology
is robust, and there won't be problems once silicon is deployed and
impossible to fix later.

(that's not to say there won't be entirely new classes of attacks coming out
of left-field in the way that Spectre surprised a lot of people, but are at
least trying to reason about the attacks we know about)

Because the costs of respinning are so high, chip design is all about
verification. Doing it in a formal sense is a step up from hand-writing or
randomly-generating tests. I don't think the industry needs convincing that
it's a good idea in abstract - it's mainly making the benefits outweigh the
costs. A lot of the work (eg in the RISC-V community) is about bringing
down those costs.

Theo

Re: (Semi-) formal methods

<s7p79m$uim$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=457&group=comp.arch.embedded#457

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Sat, 15 May 2021 12:26:30 -0700
Organization: A noiseless patient Spider
Lines: 138
Message-ID: <s7p79m$uim$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
<s7o35m$sfi$1@dont-email.me>
<167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 19:26:46 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fbf32e3585750f687207bae26fde6b55";
logging-data="31318"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19hzoXD23ma56+rr+vnS5mb"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:tyPMMtpdI8mjWLWPBhlSnLX+/x4=
In-Reply-To: <167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 19:26 UTC

On 5/15/2021 3:54 AM, Clifford Heath wrote:
> On 15/5/21 7:10 pm, Don Y wrote:
>> Unfortunately, use in such a document is not suited for "general audiences"
>
> The goal of CQL is to make the formal model suitable for (and expressed in the
> language of) anyone generally familiar with the domain being modelled.

I opted for OCL as my system is object-based, UML is relatively easy to
understand and the way things would be expressed closely mimics the
way those constraints would be imposed in the code. Any "translation"
effort would introduce other opportunities for errors to creep in.

>> because it lacks rationale for each item in the specification.
>
> Actually rationale is seldom needed. What is needed is an example of the
> scenario that is allowed or disallowed by each definition. The example is
> almost always an adequate rationalisation.

I disagree. I find many cases where I need to resort to prose to
explain why THIS implementation choice is better than THAT. Just
*stating* (or implying) that it is leaves too much to the Reader,
as an "exercise" ("Now WHY, exactly, would this be a better approach?")

For example, I had to make a decision, early on, as to whether or
not "communications" would be synchronous or asynchronous. There
are advantages and drawbacks to each approach. From a performance
standpoint, one can argue that async wins. But, from a cognitive
standpoint, sync is considerably easier for "users" (developers)
to "get right"; message and reply are temporally bound together
so the user doesn't have to, *later*, sort out which message a
subsequent reply correlates with (icky sentence structure but it's
early in the morning :< )

The fact that comms then become blocking operations means any
desire for concurrency has to be addressed with other mechanisms
(e.g., set up a thread to do the comms so the "main" thread can
keep working and make the coordination between these two -- which
now appear asynchronous -- to be more visible.)

Or, trying to explain the many ways a particular comm can fail
(e.g., what if the party on the other end never listens?
Or, *can't* listen? Or, the processor hosting it powers down?
Or...) and how the response/detection of that failure can
vary based on where in the "failure" it occurs.

>> The alternative is: an /ad hoc/ specification (with some likely incompletely
>> specified set of loose rules) *or* an *absent* specification. Each of these
>> leave gaping holes in the design that (supposedly) follows.
>
> That's precisely true. That's why analytic (formal) models are needed.

I'm not sure the models need to be mechanically verifiable. What *needs*
to happen is they need to be unambiguous and comprehensive. You should
be able to look at one (before or after the code is written) and convince
yourself that it addresses every contingency -- as well as HOW it does so
(to the appearance of other actors)

>> Again, why the resistance to adopting such a "codified" approach?
>
> Hubris, mostly. People genuinely don't see the need until enough experience has
> humbled them, and by then, their accumulated caution and tentativeness mean
> their industry sees them as dinosaurs.

"Hubris" suggests overconfidence (in their abilities). I'm not sure
that's the case.

I started looking for a "common ground" in which I could express my current
design when I "discovered" that, not only is there no such thing, but that
there isn't even a common approach (methodology) to design. It's not
a question of whether method A or method B is the more common (and, thus,
more readily recognizable to adopt in my presentation) but, that NONE OF
THE ABOVE is the clear winner!

[I couldn't even get a concensus on how to *diagram* relationships
between actors/objects just for illustrative purposes!]

This prompted the question, here.

I've been looking back over the past experiences I've had with getting
folks to "move forward" to try to see if I can identify the issue that
leads to this resistance.

Early on, I can argue that a lack of understanding for the (software)
design process led some employers to skimp in ways that they might
not have realized. E.g., when a development seat cost many thousands of
1975 dollars, you could see how an employer, new to using MPUs *in*
their products, could decide to "share" a single seat among several
developers.

Similarly, when ICEs came on the scene.

And, HLLs.

But, those issues are largely behind us as there are many "free"/cheap
tools that can make these sorts of decisions "no brainers".

I can also see how scheduling pressures could lead to a resistance
to adopt new methods that *claim* to improve productivity. I've
never been in an environment where time was allotted to explore
and learn new tools and techniques; there's another product that's
anxious to make its way to manufacturing (and YOU don't want to
be the one responsible for stalling the production line!)

I can see how fear/uncertainty can lead individuals (and organizations
as organizations are, at their heart, just individuals) to resist
change; the process you know (regardless of how bad it might be) is
safer than the process yet to BE known!

For things like specification and modeling, I can see a preception of
it as being a duplication of effort -- esp the more formally those
are expressed.

And, for some, I think an amazing lack of curiosity can explain their
clinging to The Way We Always Did It. Or, the lack of "compensation"
for the "risk" they may be taking ("Heads, you win; tails, I lose!")

*Most* of these arguments can be rationalized by "employees" -- the
excuse that THEY (personally) don't have any control over THEIR
work environment. OK, I'll avoid getting into *that* argument...

But, for folks working in more permissive environments (e.g.,
independent contractors), most of the arguments crumble. YOU can
make the time to learn a technique/tool; YOU can buy the tool;
YOU can gauge its impact on YOUR productivity; etc.

I have a lot of respect for my colleagues -- they've all got
proven track records with significant projects. Yet, they still
fall into this pattern of behavior -- clinging to past processes
instead of exploring new. To their credit, they will make an
effort to understand the approaches and technologies that *I*
pursue -- but, that's more the result of a personal relationship
(than a BUSINESS one). Yet, I never hear any epiphanies where
they exclaim "this is SO COOL"... is the pull of the familiar SO
overwhelming?

[I left the 9-to-5 world primarily so I could dabble in other
fields, techniques, etc. I have no desire to make "model 2",
especially if it will follow "process 1"!]

Re: (Semi-) formal methods

<s7pgn1$263$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=458&group=comp.arch.embedded#458

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Sat, 15 May 2021 15:07:15 -0700
Organization: A noiseless patient Spider
Lines: 77
Message-ID: <s7pgn1$263$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<yqf*720jy@news.chiark.greenend.org.uk> <s7jsr8$77r$3@dont-email.me>
<Bqf*jg5jy@news.chiark.greenend.org.uk> <s7mjh8$vcj$1@dont-email.me>
<yqf*lQ+jy@news.chiark.greenend.org.uk>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 May 2021 22:07:30 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3cd3b81f26fc860bb6882e8f42957af5";
logging-data="2243"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+Fz+BELXaMdFWR5c51T731"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:yL9HZksra9/QERtt/ivlOVBL/P0=
In-Reply-To: <yqf*lQ+jy@news.chiark.greenend.org.uk>
Content-Language: en-US
 by: Don Y - Sat, 15 May 2021 22:07 UTC

On 5/15/2021 4:02 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote:
>> Understood. Tools fit the application domains for which they were designed.
>>
>> How did *adoption* of the tool come to pass? Was it "mandated" by corporate
>> policy? Something <someone> stumbled on, played with and then "pitched"
>> to management/peers? Mandated by your industry? etc.
>>
>> [Just because a tool "makes sense" -- logically or economically -- doesn't
>> mean it will be adopted, much less *embraced*!]
>
> We're a university research lab. We developed the tool in response to two
> trends:
>
> - growing complexity of systems and the increasing prevalence of bugs in
> implementation (for example in memory coherency subsystems).
>
> - proposing security extensions to architectures and wanting to be able to
> show that what we've proposed doesn't have any loopholes in it. It provides
> confidence to us and to people adopting the technology that the technology
> is robust, and there won't be problems once silicon is deployed and
> impossible to fix later.

OK. Both make sense. And, both are hard (if not impossible) to "fix"
at layers *above* the hardware.

The next, most practical, question is: how do you encourage its adoption?
Publishing papers is what professors/grad students "do". That's
different from actually getting folks to *use* something that you've
developed/written about.

(a casual examination of the amount of "stuff" that has come out of
academia and "gone nowhere" -- despite some value! -- should make
this evident)

> (that's not to say there won't be entirely new classes of attacks coming out
> of left-field in the way that Spectre surprised a lot of people, but are at
> least trying to reason about the attacks we know about)
>
> Because the costs of respinning are so high, chip design is all about
> verification. Doing it in a formal sense is a step up from hand-writing or
> randomly-generating tests. I don't think the industry needs convincing that
> it's a good idea in abstract - it's mainly making the benefits outweigh the
> costs. A lot of the work (eg in the RISC-V community) is about bringing
> down those costs.

Understood. In the past, I've had to rely on "good eyes" to spot problems
in designs. Folks tend to only test how they *think* the design SHOULD
perform. So, they often omit checking for things that they don't imagine
it (mis?)doing.

<do something; witness crash>
"What did you just do?"
"This..."
"You're not supposed to do that!"
"Then why did you/it LET ME? Did I break some *law*???"

[Thankfully, I have a nack for identifying MY "assumptions" and the
liabilities that they bring to a design]

A suitably aggressive tool can avoid this bias and just hammer at every
nit it can algorithmically deduce/exploit.

A colleague designed a video scaler for a printer. When I started poking at
it with real numbers, I discovered cases where the PHYSICAL image size
produced on a B-size page was actually SMALLER than that produced on an
A-size page (presumably, you'd print on larger paper to get a larger image!).

Ooops!

Given the number of variations in how the interface could be configured,
he'd never have been able to exhaustively test all cases. So, my observation
was just serendipitous.

OTOH, *seeing* what I'd uncovered gave him cause to look more carefully
at his implementation *before* sending it off to fab (which would have cost
money AND calendar time -- leading to a delayed market introduction).

Re: (Semi-) formal methods

<167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=459&group=comp.arch.embedded#459

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me> <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com> <s7nk3b$d0m$1@dont-email.me> <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com> <s7o35m$sfi$1@dont-email.me> <167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com> <s7p79m$uim$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Sun, 16 May 2021 11:41:32 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s7p79m$uim$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>
Lines: 158
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!tr1.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::44.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Sun, 16 May 2021 01:41:35 +0000
X-Received-Bytes: 8285
Organization: theCubeNet - www.thecubenet.com
X-Complaints-To: abuse@thecubenet.com
 by: Clifford Heath - Sun, 16 May 2021 01:41 UTC

On 16/5/21 5:26 am, Don Y wrote:
> On 5/15/2021 3:54 AM, Clifford Heath wrote:
>> On 15/5/21 7:10 pm, Don Y wrote:
>>> Unfortunately, use in such a document is not suited for "general
>>> audiences"
>>
>> The goal of CQL is to make the formal model suitable for (and
>> expressed in the language of) anyone generally familiar with the
>> domain being modelled.
>
> I opted for OCL as my system is object-based, UML is relatively easy to
> understand and the way things would be expressed closely mimics the
> way those constraints would be imposed in the code.  Any "translation"
> effort would introduce other opportunities for errors to creep in.

It's very difficult to teach non-programmers to read OCL. But I agree on
the need for code generation directly from the model, without
translation. That's what CQL does too.

>> Actually rationale is seldom needed. What is needed is an example of
>> the scenario that is allowed or disallowed by each definition. The
>> example is almost always an adequate rationalisation.
>
> I disagree.  I find many cases where I need to resort to prose to
> explain why THIS implementation choice is better than THAT.

Yes, where that is needed, CQL provides context-notes too. In fact I
select four specific categories of rationale ("so that", "because", "as
opposed to" and "to avoid"), with optional annotations saying who agreed
and when.

> For example, I had to make a decision, early on, as to whether or
> not "communications" would be synchronous or asynchronous.  There
> are advantages and drawbacks to each approach.  From a performance
> standpoint, one can argue that async wins.  But, from a cognitive
> standpoint, sync is considerably easier for "users" (developers)
> to "get right"; message and reply are temporally bound together
> so the user doesn't have to, *later*, sort out which message a
> subsequent reply correlates with (icky sentence structure but it's
> early in the morning  :< )

Yes, I'm well familiar with that problem. Best decade of my working life
was building a development tool that exclusively used message passing.
For the most part it's amazingly liberating, but sometimes frustrating.

>> That's precisely true. That's why analytic (formal) models are needed.
>
> I'm not sure the models need to be mechanically verifiable.

Even without verification, the model must only make rules that are *in
principle* machine-verifiable. If a rule is not verifiable, it's just
waffle with no single logical meaning. If it has a single logical
meaning, it is in principle machine-verifiable.

>  What *needs*
> to happen is they need to be unambiguous and comprehensive.

Comprehensive is impossible. There's always a possibility for more
detail in any real-world system. But unambiguous? Yes, that requires
that it is a formal part of a formal system which allows its meaning to
be definitively stated. That is, for any scenario, there exists a
decision procedure which can determine whether that scenario is allowed
or is disallowed (this is what is meant when a logical system is termed
"decidable").

>  You should
> be able to look at one (before or after the code is written) and convince
> yourself that it addresses every contingency

It's a great goal, but it is *in principle* impossible. Correctness of
every contingency requires that the model matches the "real world", and
Godel's theorem shows that it's impossible to prove that.

>>> Again, why the resistance to adopting such a "codified" approach?
>>
>> Hubris, mostly. People genuinely don't see the need until enough
>> experience has humbled them, and by then, their accumulated caution
>> and tentativeness mean their industry sees them as dinosaurs.
>
> "Hubris" suggests overconfidence (in their abilities).  I'm not sure
> that's the case.
>
> I started looking for a "common ground" in which I could express my current
> design

Fact-based modelling uses language as an access point to people's mental
models, by analysing "plausible utterances" or "speech acts" for their
logical intent, and building a formal model that captures the domain
*using their own terms and phrases*.

Poor though it is, there exists no better tool than natural language to
explore and express common ground. CQL provides a two-way bridge between
that and formal logic, so that any mathematically formal statement can
be unambiguously expressed using natural sentences, and every fact in
the domain can be expressed using at least one agreed sentence using a
restricted natural grammar that is also mathematically formal (meaning,
unambiguously parseable to a logical expression).

> when I "discovered" that, not only is there no such thing,

Each model needs to be formulated by agreement in each case. The only
way to reach agreement is to express scenarios and formalise ways of
expressing them, so that any acceptable statement can be analysed for
its logical intent.

This works because every functioning business already has ways to talk
about everything that matters to it. Fact-based modeling captures those
expressions and formalises them, using their own words to express the
result, so agreement can be reached. It's little use to formalise a rule
in a way that cannot be verified by the people who proposed it - one
cannot reach agreement that way. Many MANY development failures fall
into the trap of "but you said... no but I meant....!", or "I didn't say
that because it's just common sense! What kind of fool are you?"

> I've been looking back over the past experiences I've had with getting
> folks to "move forward" to try to see if I can identify the issue that
> leads to this resistance.

"Every man's way is right in his own eyes" - Proverbs 21:2

People can't see the flaws in their own logic, because their logic is
flawed. They resist methodical attempts to correct them, because they're
already "right".

> I've
> never been in an environment where time was allotted to explore
> and learn new tools and techniques;

I know a number of companies that implement "10% time", for employees to
explore any technology or personal projects they feel might be relevant
to the business (or to their ability to contribute to it). I think
Google is one of these, in fact, though my examples are closer to home.

> For things like specification and modeling, I can see a preception of
> it as being a duplication of effort -- esp the more formally those
> are expressed.

Unfortunately a lot of companies view testing in the same way. As if it
wasn't possible for them to make a mistake.

> And, for some, I think an amazing lack of curiosity can explain their
> clinging to The Way We Always Did It.  Or, the lack of "compensation"
> for the "risk" they may be taking ("Heads, you win; tails, I lose!")

Folk who have been "lucky" a few times tend to become the "golden child"
and get promoted. Once in senior positions they're much more likely to
reject techniques which could discover that "the emperor has no clothes"

> I have a lot of respect for my colleagues -- they've all got
> proven track records with significant projects.  Yet, they still
> fall into this pattern of behavior -- clinging to past processes
> instead of exploring new.

I look forward to hearing of your experiences with TLA+, Alloy, or CQL.
I promise that it will be worth your effort.

Clifford Heath.

Re: (Semi-) formal methods

<s7qi0g$413$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=460&group=comp.arch.embedded#460

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Sun, 16 May 2021 00:35:27 -0700
Organization: A noiseless patient Spider
Lines: 239
Message-ID: <s7qi0g$413$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
<s7o35m$sfi$1@dont-email.me>
<167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
<s7p79m$uim$1@dont-email.me>
<167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sun, 16 May 2021 07:35:45 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3cd3b81f26fc860bb6882e8f42957af5";
logging-data="4131"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/s8qJc2rY0lExmvLOx+wpZ"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:w9xZWbtnhfAR2o+G/yLvPxzpWwY=
In-Reply-To: <167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Sun, 16 May 2021 07:35 UTC

On 5/15/2021 6:41 PM, Clifford Heath wrote:
> On 16/5/21 5:26 am, Don Y wrote:
>> On 5/15/2021 3:54 AM, Clifford Heath wrote:
>>> On 15/5/21 7:10 pm, Don Y wrote:
>>>> Unfortunately, use in such a document is not suited for "general audiences"
>>>
>>> The goal of CQL is to make the formal model suitable for (and expressed in
>>> the language of) anyone generally familiar with the domain being modelled.
>>
>> I opted for OCL as my system is object-based, UML is relatively easy to
>> understand and the way things would be expressed closely mimics the
>> way those constraints would be imposed in the code. Any "translation"
>> effort would introduce other opportunities for errors to creep in.
>
> It's very difficult to teach non-programmers to read OCL. But I agree on the
> need for code generation directly from the model, without translation. That's
> what CQL does too.

My target audience is programmers.

>>> Actually rationale is seldom needed. What is needed is an example of the
>>> scenario that is allowed or disallowed by each definition. The example is
>>> almost always an adequate rationalisation.
>>
>> I disagree. I find many cases where I need to resort to prose to
>> explain why THIS implementation choice is better than THAT.
>
> Yes, where that is needed, CQL provides context-notes too. In fact I select
> four specific categories of rationale ("so that", "because", "as opposed to"
> and "to avoid"), with optional annotations saying who agreed and when.

I present my descriptions in "multimedia prose" so I can illustrate
(and animate) to better convey the intent.

In some domains, "text" is just a terrible choice for explaining what
you're doing (e.g., speech synthesis, gesture recognition, etc.).
It's considerably easier to emit sounds or animate graphics (in these
mentioned examples) than to try to describe what you're addressing.

>> For example, I had to make a decision, early on, as to whether or
>> not "communications" would be synchronous or asynchronous. There
>> are advantages and drawbacks to each approach. From a performance
>> standpoint, one can argue that async wins. But, from a cognitive
>> standpoint, sync is considerably easier for "users" (developers)
>> to "get right"; message and reply are temporally bound together
>> so the user doesn't have to, *later*, sort out which message a
>> subsequent reply correlates with (icky sentence structure but it's
>> early in the morning :< )
>
> Yes, I'm well familiar with that problem. Best decade of my working life was
> building a development tool that exclusively used message passing.
> For the most part it's amazingly liberating, but sometimes frustrating.

From the comments I've received from colleagues using my codebase,
the biggest problems seem to be related to (true) concurrency and
the possibility of a remote host failing while the message is in transit.
Folks seem to be used to "local" results in short order (transport delays
not being significant even in an IPC)

>>> That's precisely true. That's why analytic (formal) models are needed.
>>
>> I'm not sure the models need to be mechanically verifiable.
>
> Even without verification, the model must only make rules that are *in
> principle* machine-verifiable. If a rule is not verifiable, it's just waffle
> with no single logical meaning. If it has a single logical meaning, it is in
> principle machine-verifiable.

Yes. But *getting* such a tool (or requiring its existence before adopting
a model strategy) can be prohibitive.

>> What *needs*
>> to happen is they need to be unambiguous and comprehensive.
>
> Comprehensive is impossible.

"Comprehensive" only has to apply to the world-view seen through the
interface. If you're dealing with a particular actor/object/server,
all you have to do is be able to define EVERY possible outcome that
a client could experience using that interface.

If the sky turns yellow and every cat on the planet dies... <shrug>
(likely this isn't pertinent to any interface)

OTOH, if a process can die while servicing a request, or run out
of resources, or encounter invalid operands, or... then each of
those possibilities have to be enumerated.

Much of the additional cruft (in my world) comes from the fact
that the request is executing "elsewhere" (even if on the same
host) while YOUR code appears to be running correctly; there's
no guarantee that the request is executing AT ALL.

> There's always a possibility for more detail in
> any real-world system. But unambiguous? Yes, that requires that it is a formal
> part of a formal system which allows its meaning to be definitively stated.
> That is, for any scenario, there exists a decision procedure which can
> determine whether that scenario is allowed or is disallowed (this is what is
> meant when a logical system is termed "decidable").
>
>> You should
>> be able to look at one (before or after the code is written) and convince
>> yourself that it addresses every contingency
>
> It's a great goal, but it is *in principle* impossible. Correctness of every
> contingency requires that the model matches the "real world", and Godel's
> theorem shows that it's impossible to prove that.

Again, it only has to match the portion of the real world visible to
the interface in question.

A filesystem interface doesn't have to address the possibility of
the polar ice caps melting...

>>>> Again, why the resistance to adopting such a "codified" approach?
>>>
>>> Hubris, mostly. People genuinely don't see the need until enough experience
>>> has humbled them, and by then, their accumulated caution and tentativeness
>>> mean their industry sees them as dinosaurs.
>>
>> "Hubris" suggests overconfidence (in their abilities). I'm not sure
>> that's the case.
>>
>> I started looking for a "common ground" in which I could express my current
>> design
>> when I "discovered" that, not only is there no such thing,

You've missed the point. I was addressing the point that modeling, itself,
is relatively uncommon (at least in "these circles"). So, trying to find
some common subset that everyone (most practitioners) were using was
pointless.

If no one speaks Esperanto, then it is foolish to present your documentation
*in* Esperanto!

>> I've been looking back over the past experiences I've had with getting
>> folks to "move forward" to try to see if I can identify the issue that
>> leads to this resistance.
>
> "Every man's way is right in his own eyes" - Proverbs 21:2
>
> People can't see the flaws in their own logic, because their logic is flawed.
> They resist methodical attempts to correct them, because they're already "right".

That's more pessimistic than I -- a cynic -- would claim.

When I approached my colleagues re: this topic, no one tried to
defend their current practices. I think they all realize they
*could* be doing things "better". This led to my contemplation of
why they *aren't* moving in those directions.

It's like the guy who KNOWS he should be backing up his computer...
yet doesn't. Why????

>> I've
>> never been in an environment where time was allotted to explore
>> and learn new tools and techniques;
>
> I know a number of companies that implement "10% time", for employees to
> explore any technology or personal projects they feel might be relevant to the
> business (or to their ability to contribute to it). I think Google is one of
> these, in fact, though my examples are closer to home.

Yes, but 10% of 40 hours isn't a helluvalot of time. I would imagine
other things chip away at that time.

I've seen companies budget for "reading technical journals/rags", etc.
But, unless you're really aggressive with your time management, it's
unlikely that a few hours a week is going to amount to much -- other
than priming you for your after-work pursuit of the problem (on YOUR time)

>> For things like specification and modeling, I can see a preception of
>> it as being a duplication of effort -- esp the more formally those
>> are expressed.
>
> Unfortunately a lot of companies view testing in the same way. As if it wasn't
> possible for them to make a mistake.

I think everyone (management) would LOVE to test. If it didn't take any
TIME! I don't think the same is true of developers! Most seem to
consider testing "tedious" -- not very fulfilling. Hence they only test
for what they KNOW the code/product should do!


Click here to read the complete article
Re: (Semi-) formal methods

<1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=483&group=comp.arch.embedded#483

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me> <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com> <s7nk3b$d0m$1@dont-email.me> <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com> <s7o35m$sfi$1@dont-email.me> <167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com> <s7p79m$uim$1@dont-email.me> <167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com> <s7qi0g$413$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Wed, 2 Jun 2021 12:03:28 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s7qi0g$413$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com>
Lines: 117
Path: i2pn2.org!i2pn.org!aioe.org!feeder1.feed.usenet.farm!feed.usenet.farm!tr2.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::43.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Wed, 2 Jun 2021 02:03:31 +0000
X-Received-Bytes: 6487
X-Complaints-To: abuse@thecubenet.com
Organization: theCubeNet - www.thecubenet.com
 by: Clifford Heath - Wed, 2 Jun 2021 02:03 UTC

On 16/5/21 5:35 pm, Don Y wrote:
> On 5/15/2021 6:41 PM, Clifford Heath wrote:
>> On 16/5/21 5:26 am, Don Y wrote:
>>> On 5/15/2021 3:54 AM, Clifford Heath wrote:
>>>> On 15/5/21 7:10 pm, Don Y wrote:
>>>>> Unfortunately, use in such a document is not suited for "general
>>>>> audiences"
>>>>
>>>> The goal of CQL is to make the formal model suitable for (and
>>>> expressed in the language of) anyone generally familiar with the
>>>> domain being modelled.
>>>> Actually rationale is seldom needed. What is needed is an example of
>>>> the scenario that is allowed or disallowed by each definition. The
>>>> example is almost always an adequate rationalisation.
>>>
>>> I disagree.  I find many cases where I need to resort to prose to
>>> explain why THIS implementation choice is better than THAT.
>>
>> Yes, where that is needed, CQL provides context-notes too. In fact I
>> select four specific categories of rationale ("so that", "because",
>> "as opposed to" and "to avoid"), with optional annotations saying who
>> agreed and when.
>
> I present my descriptions in "multimedia prose" so I can illustrate
> (and animate) to better convey the intent.

All that is needed is to allow the viewer to get to the "Aha!" moment
where they see why the alternative will fail. Do whatever you have to do
to achieve that, and you have your rationale. It will vary with the
situation, and with the audience.

>> Even without verification, the model must only make rules that are *in
>> principle* machine-verifiable. If a rule is not verifiable, it's just
>> waffle with no single logical meaning. If it has a single logical
>> meaning, it is in principle machine-verifiable.
>
> Yes.  But *getting* such a tool (or requiring its existence before adopting
> a model strategy) can be prohibitive.
>> There's always a possibility for more detail in any real-world system.

>>>>> Again, why the resistance to adopting such a "codified" approach?
>>>> Hubris, mostly. People genuinely don't see the need until enough
>>>> experience has humbled them, and by then, their accumulated caution
>>>> and tentativeness mean their industry sees them as dinosaurs.
>>>
>>> "Hubris" suggests overconfidence (in their abilities).  I'm not sure
>>> that's the case.
>>>
>>> I started looking for a "common ground" in which I could express my
>>> current design when I "discovered" that, not only is there no such thing,
>
> You've missed the point.  I was addressing the point that modeling, itself,
> is relatively uncommon (at least in "these circles").  So, trying to find
> some common subset that everyone (most practitioners) were using was
> pointless.
>
> If no one speaks Esperanto, then it is foolish to present your
> documentation *in* Esperanto!

In relation to software, at least, every modeling language has been a
private language shared only (or mainly) by systems architects. They're
all Esperanto, of one kind or another. (ER diagramming has sometimes
been useful, and occasionally even UML, but usually not)

As such, it serves only for documenting the system *as designed*, and
can provide no help to a non-expert in identifying flaws where the
result would not match the need (as opposed to not working correctly
within its own frame of reference).

Because "modelling" has always been subject to this failure, it is seen
as a pointless exercise. Delivered software is likely to work "as
designed" yet still mis-match the problem because the design was
mis-targeted, whether it was modelled or was not.

The solution to this is good modelling tools that can communicate to
*everyone*, not just to programmers. And that's what I spent a decade
trying to build.

> When I approached my colleagues re: this topic, no one tried to
> defend their current practices.  I think they all realize they
> *could* be doing things "better".  This led to my contemplation of
> why they *aren't* moving in those directions.

It's easier to "stay in town" where it's comfortable, than to go
exploring in the wilderness. It's wilderness because there is no
adoption, and there's no adoption not because no-one has been there, but
because they didn't build roads and towns there yet.

>> I know a number of companies that implement "10% time",
> Yes, but 10% of 40 hours isn't a helluvalot of time.

Half a day a week seems like quite a lot to me. If an employee doing
that can't prove to me that they've discovered something worthy of a
bigger investment, then I don't believe they have.

At one company, I spent 18 months trying to evangelise the business need
for a new technology I'd envisaged. Eventually someone told my manager
"just give him 2 weeks to prototype it!", and I did. The effect was
astounding - the entire company (110 people) dropped everything else
they were doing to work on producing a new product based on my idea.
That product brought in well over a hundred million dollars over the
next decade.

>> I look forward to hearing of your experiences with TLA+, Alloy, or CQL.
>> I promise that it will be worth your effort.
>
> It's unlikely that I will try any of them!  This is my last "electronics"
> project (50 years in a field seems like "enough"; time to pursue OTHER
> interests!)

And that is why I'm sometimes reluctant to engage in these conversations
with you, Don. You're the one asking "why does nobody try this", but
even now you have time to explore (without the demands of delivering a
result), you're unwilling to do more than talk about that.

Clifford Heath.

Re: (Semi-) formal methods

<s974lf$vm4$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=484&group=comp.arch.embedded#484

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Tue, 1 Jun 2021 22:23:44 -0700
Organization: A noiseless patient Spider
Lines: 386
Message-ID: <s974lf$vm4$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
<s7o35m$sfi$1@dont-email.me>
<167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
<s7p79m$uim$1@dont-email.me>
<167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>
<s7qi0g$413$1@dont-email.me>
<1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 2 Jun 2021 05:23:59 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="c7568f508d05cad150e1afa65fe148d1";
logging-data="32452"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19GDf5gaDFh17fU/itazqm3"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:vIwIuFANO//fpqElbRwU5Q2IVNA=
In-Reply-To: <1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Wed, 2 Jun 2021 05:23 UTC

On 6/1/2021 7:03 PM, Clifford Heath wrote:
> On 16/5/21 5:35 pm, Don Y wrote:
>> On 5/15/2021 6:41 PM, Clifford Heath wrote:
>>> On 16/5/21 5:26 am, Don Y wrote:
>>>> On 5/15/2021 3:54 AM, Clifford Heath wrote:
>>>>> On 15/5/21 7:10 pm, Don Y wrote:
>>>>>> Unfortunately, use in such a document is not suited for "general audiences"
>>>>>
>>>>> The goal of CQL is to make the formal model suitable for (and expressed in
>>>>> the language of) anyone generally familiar with the domain being modelled.
>>>>> Actually rationale is seldom needed. What is needed is an example of the
>>>>> scenario that is allowed or disallowed by each definition. The example is
>>>>> almost always an adequate rationalisation.
>>>>
>>>> I disagree. I find many cases where I need to resort to prose to
>>>> explain why THIS implementation choice is better than THAT.
>>>
>>> Yes, where that is needed, CQL provides context-notes too. In fact I select
>>> four specific categories of rationale ("so that", "because", "as opposed to"
>>> and "to avoid"), with optional annotations saying who agreed and when.
>>
>> I present my descriptions in "multimedia prose" so I can illustrate
>> (and animate) to better convey the intent.
>
> All that is needed is to allow the viewer to get to the "Aha!" moment where
> they see why the alternative will fail. Do whatever you have to do to achieve
> that, and you have your rationale. It will vary with the situation, and with
> the audience.

I've found that people tend to "lack imagination" when it comes to
things in which they aren't DEEPLY invested. They often fail to
see ("go looking for") aspects of a design that aren't superficially
obvious. This evidenced by how many folks only test their designs
with inputs they EXPECT to encounter (instead of imagining the larger
set of inputs *possible*).

So, I try to develop "interactions" that let the "reader" see what
I'm trying to illustrate -- and, then, coach them into pondering
"what ifs" that they've NOT likely imagined and show how those
win/fail in different alternatives.

With interactive presentations, I can literally tell them to "do X"
and know that (if they do), the presentation will clearly show
the issue that I would, otherwise, find tedious to explain in prose.

>>>>>> Again, why the resistance to adopting such a "codified" approach?
>>>>> Hubris, mostly. People genuinely don't see the need until enough
>>>>> experience has humbled them, and by then, their accumulated caution and
>>>>> tentativeness mean their industry sees them as dinosaurs.
>>>>
>>>> "Hubris" suggests overconfidence (in their abilities). I'm not sure
>>>> that's the case.
>>>>
>>>> I started looking for a "common ground" in which I could express my current
>>>> design when I "discovered" that, not only is there no such thing,
>>
>> You've missed the point. I was addressing the point that modeling, itself,
>> is relatively uncommon (at least in "these circles"). So, trying to find
>> some common subset that everyone (most practitioners) were using was
>> pointless.
>>
>> If no one speaks Esperanto, then it is foolish to present your documentation
>> *in* Esperanto!
>
> In relation to software, at least, every modeling language has been a private
> language shared only (or mainly) by systems architects. They're all Esperanto,
> of one kind or another. (ER diagramming has sometimes been useful, and
> occasionally even UML, but usually not)
>
> As such, it serves only for documenting the system *as designed*, and can

That's exactly my goal. I'm looking to "translate" my design into
form(s) that may be more easily recognizable -- to some "significant"
group of readers.

For example, one can design a grammar with totally /ad hoc/ methods.
But, presenting it a BNF goes a long way to clarifying it to "new
readers" -- regardless of how it came about (or was implemented).

> provide no help to a non-expert in identifying flaws where the result would not
> match the need (as opposed to not working correctly within its own frame of
> reference).

Different goal.

A "non-expert" reading the BNF of a grammar wouldn't be able to glean
much about how it *could* be implemented or inconsistencies in any
potential implementation. But, he *could* construct a valid sentence
with just that BNF (and not worry about how it gets parsed).

> Because "modelling" has always been subject to this failure, it is seen as a
> pointless exercise. Delivered software is likely to work "as designed" yet
> still mis-match the problem because the design was mis-targeted, whether it was
> modelled or was not.
>
> The solution to this is good modelling tools that can communicate to
> *everyone*, not just to programmers. And that's what I spent a decade trying to
> build.

You're trying to solve a different problem than I.

I agree with your points -- in *that* application domain.

>> When I approached my colleagues re: this topic, no one tried to
>> defend their current practices. I think they all realize they
>> *could* be doing things "better". This led to my contemplation of
>> why they *aren't* moving in those directions.
>
> It's easier to "stay in town" where it's comfortable, than to go exploring in
> the wilderness. It's wilderness because there is no adoption, and there's no
> adoption not because no-one has been there, but because they didn't build roads
> and towns there yet.

I don't think "ease" or "comfort" is the issue. Many of my colleagues
are involved with very novel designs and application domains. They
are almost always "treking in the wilderness".

But, they aren't likely to add additional uncertainty to their efforts
by tackling novel design techniques on top of a novel application
(or application domain). There's a limit as to how much "risk"
one can take on -- especially if you are answerable to "others"
(the folks who pay the bills).

I have historically taken on lots of "new experience" because it
was something I could fold into *my* time... I could decide to
"eat" the cost of learning a new technology "on my dime" as long
as I'd budgeted (timewise) to meat my completion estimates for
clients. *They* don't care if I move all of my development
tools to UN*X -- as long as they can support my completed
work with their *Windows* toolchains.

[I.e., I bear the cost of assuming both worlds work -- the UN*X
domain for me and the Windows domain for them]

But, others may see no point in moving to a different hosting
platform: "What's wrong with Windows?" Should I fault them for
"staying in town"?

>>> I know a number of companies that implement "10% time",
>> Yes, but 10% of 40 hours isn't a helluvalot of time.
>
> Half a day a week seems like quite a lot to me. If an employee doing that can't
> prove to me that they've discovered something worthy of a bigger investment,
> then I don't believe they have.

Four hours a week is nothing.

A colleague, many years ago, was assessing the effort for a particular
task. He made the off-hand comment: "You can't do ANYTHING in 8 hours!"
Which warranted a chuckle.

But, in hindsight, there's a sort of truism, there.

There are costs to starting and stopping activities. Folks who say
"10% of your time" are obviously TRACKING time. How much time am
I allotted to handle my daily correspondence (which may be distributed
across the day and not neatly bundled in a "lump")? How much time
for project meetings? How much time to browse trade magazines
to "keep current" with product offerings? Ditto published works?
Do I have a separate account to charge time to handle questions
from the manufacturing engineer re: my design? What if I need
to visit the toilet? Do I have an account against which to charge
my TIMEKEEPING time?

Four hours gets frittered away -- unless you start nickel and diming
your "real" projects with the time "lost" to these other incidentals.

Even with no one driving my time on a daily basis (self-employed),
it is still amazing how quickly a day "disappears". A piece of
test equipment needs repair/calibration/updating, ditto for a
piece of software, a battery in a UPS dies and a replacement needs
to be ordered -- and eventually installed. Etc.


Click here to read the complete article
Re: (Semi-) formal methods

<1684c4474360859e$1$1356503$70dd7a6b@news.thecubenet.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=485&group=comp.arch.embedded#485

 copy link   Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Newsgroups: comp.arch.embedded
References: <s7fara$f23$1@dont-email.me> <167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com> <s7nk3b$d0m$1@dont-email.me> <167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com> <s7o35m$sfi$1@dont-email.me> <167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com> <s7p79m$uim$1@dont-email.me> <167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com> <s7qi0g$413$1@dont-email.me> <1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com> <s974lf$vm4$1@dont-email.me>
From: no.s...@please.net (Clifford Heath)
Date: Wed, 2 Jun 2021 22:39:34 +1000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
MIME-Version: 1.0
In-Reply-To: <s974lf$vm4$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <1684c4474360859e$1$1356503$70dd7a6b@news.thecubenet.com>
Lines: 126
Path: i2pn2.org!i2pn.org!news.swapon.de!news.uzoreto.com!feeder1.feed.usenet.farm!feed.usenet.farm!fdc3.netnews.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!2a07:8080:119:fe::44.MISMATCH!news.thecubenet.com!not-for-mail
NNTP-Posting-Date: Wed, 2 Jun 2021 12:39:36 +0000
X-Received-Bytes: 6774
Organization: theCubeNet - www.thecubenet.com
X-Complaints-To: abuse@thecubenet.com
 by: Clifford Heath - Wed, 2 Jun 2021 12:39 UTC

On 2/6/21 3:23 pm, Don Y wrote:
> On 6/1/2021 7:03 PM, Clifford Heath wrote:
>> On 16/5/21 5:35 pm, Don Y wrote:
>>> On 5/15/2021 6:41 PM, Clifford Heath wrote:
>>>> Yes, where that is needed, CQL provides context-notes too >>> I present my descriptions in "multimedia prose" so I can illustrate
>>> (and animate) to better convey the intent.
>>
>> All that is needed is to allow the viewer to get to the "Aha!" moment
>> where they see why the alternative will fail. Do whatever you have to
>> do to achieve that, and you have your rationale. It will vary with the
>> situation, and with the audience.
>
> I've found that people tend to "lack imagination" when it comes to
> things in which they aren't DEEPLY invested.

It's almost always the case that a simple "if we have *that*, and *this*
happens, and we respond like *this*, this would be bad, yeah?" is enough
to cover 99% of such situations. But as I said, every case is different,
and I make no criticism of the way you do things. Anyhow, a minor point.

>> As such, it serves only for documenting the system *as designed*, and can
> That's exactly my goal.  I'm looking to "translate" my design into
> form(s) that may be more easily recognizable -- to some "significant"
> group of readers.

No worries. That's what systems architecture languages are for. They
only seem to get adopted where they're mandated though.

>> provide no help to a non-expert in identifying flaws where the result
>> would not match the need (as opposed to not working correctly within
>> its own frame of reference).
> Different goal.

Agreed. But the model I produce is *also* compilable to working code,
and can also be generated into a machine reasoning framework (program
prover or SAT solver) for formal analysis. My novel contribution is
doing that in a form of language which is comprehensible to "lay people"
without training.

>> The solution to this is good modelling tools that can communicate to
>> *everyone*, not just to programmers. And that's what I spent a decade
>> trying to build.
>
> You're trying to solve a different problem than I.
>
> I agree with your points -- in *that* application domain.

Every problem in every domain must be defined before it can be solved.
If the definition is not understood by those who have to live with the
solution, then it *will* be mis-defined. That is the sad fact behind the
software industry's dismal record.

> I don't think "ease" or "comfort" is the issue.  Many of my colleagues
> are involved with very novel designs and application domains.  They
> are almost always "treking in the wilderness".
>
> But, they aren't likely to add additional uncertainty to their efforts

And there's the nub. They see these "unproven" technologies as adding
uncertainty, where the reality is that they exist to *reduce
uncertainty. The truth? They're afraid the formal analysis will show
everyone how wrong they are, and have always been.

>>>> I look forward to hearing of your experiences with TLA+, Alloy, or CQL.
>>>> I promise that it will be worth your effort.
>>>
>>> It's unlikely that I will try any of them!  This is my last
>>> "electronics"
>>> project (50 years in a field seems like "enough"; time to pursue OTHER
>>> interests!)
>>
>> And that is why I'm sometimes reluctant to engage in these
>> conversations with you, Don. You're the one asking "why does nobody
>> try this", but even now you
>
> You've misread my intent.  I am not ACCUSING anyone.  Rather, I am
> trying to
> see how people have AVOIDED "doing this".  How are folks designing
> products if
> they aren't writing specifications, modeling behaviors, quantifying market
> requirements, etc.?  (if they ARE doing those things, then WHICH are they
> doing??)

Good question. I agree with your thoughts. But that has nothing to do
with what I was getting at.

>> have time to explore (without the demands of delivering a result), you're
> Who says I don't have to "deliver a result"?
>> unwilling to do more than talk about that.
> Who says I've not "ventured into the uncharted wilderness"?

No-one. Certainly not me. But you've said you're effectively retiring.
To me that means you don't have to "deliver a result" any more.
But it also means that you can take even more time to explore, if you
like to go even further from the well-trodden paths, so I suggested a
few interesting paths that you might like to explore in your dotage.
Perhaps learn something that you could communicate to help less
experienced folk. So I was a bit surprised when you said you were
unlikely to do that.

Instead you blather on about the many things in your past. Guess what?
Lots of us have many varied experiences in our past. You'd be surprised
how widely my interests have strayed off the beaten tracks - I'm also a
life-long explorer. But this is not about me, or about you, it's about
how the industries we work in could do even better than we could, and
what we could yet learn to help them do that. I'd still like to add to
my legacy, and I hope you would too.

Not just raise a long discussion leading to interesting areas to
explore, then announce that it was all useless because you don't intend
to explore any more.

> All of these are "wilderness" areas.  All of them took time to research,
> implement and evaluate.
>
> So, I guess I have a different idea of "having time to explore" than
> you do!

But that was all in the past. Apparently you no longer have the desire
to explore. That seems to be what you said anyhow. Correct me if I've
misread that:

> "It's unlikely that I will try any of them! This is my last
> "electronics" project (50 years in a field seems like "enough""

Clifford Heath

Re: (Semi-) formal methods

<s98a13$ml4$1@dont-email.me>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=487&group=comp.arch.embedded#487

 copy link   Newsgroups: comp.arch.embedded
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: blockedo...@foo.invalid (Don Y)
Newsgroups: comp.arch.embedded
Subject: Re: (Semi-) formal methods
Date: Wed, 2 Jun 2021 09:01:26 -0700
Organization: A noiseless patient Spider
Lines: 156
Message-ID: <s98a13$ml4$1@dont-email.me>
References: <s7fara$f23$1@dont-email.me>
<167f224f71eaadb2$1$2112880$6edd646a@news.thecubenet.com>
<s7nk3b$d0m$1@dont-email.me>
<167f2f5a945a8023$1$2262039$72dd786b@news.thecubenet.com>
<s7o35m$sfi$1@dont-email.me>
<167f3814b72711a5$1$1356503$70dd7a6b@news.thecubenet.com>
<s7p79m$uim$1@dont-email.me>
<167f68816b02e386$1$1356503$70dd7a6b@news.thecubenet.com>
<s7qi0g$413$1@dont-email.me>
<1684a19157d3c812$1$2262039$72dd786b@news.thecubenet.com>
<s974lf$vm4$1@dont-email.me>
<1684c4474360859e$1$1356503$70dd7a6b@news.thecubenet.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 2 Jun 2021 16:01:40 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="c7568f508d05cad150e1afa65fe148d1";
logging-data="23204"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19oCj5Ev2bvwZUfgbfy6yh8"
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101
Thunderbird/52.1.1
Cancel-Lock: sha1:WdFVraLpk2YH66hAGX11bc1/l5E=
In-Reply-To: <1684c4474360859e$1$1356503$70dd7a6b@news.thecubenet.com>
Content-Language: en-US
 by: Don Y - Wed, 2 Jun 2021 16:01 UTC

On 6/2/2021 5:39 AM, Clifford Heath wrote:

>> I don't think "ease" or "comfort" is the issue. Many of my colleagues
>> are involved with very novel designs and application domains. They
>> are almost always "treking in the wilderness".
>>
>> But, they aren't likely to add additional uncertainty to their efforts
>
> And there's the nub. They see these "unproven" technologies as adding
> uncertainty, where the reality is that they exist to *reduce uncertainty. The

They can only *potentially* "reduce uncertainty" after they are understood
and "mastered" (to whatever degree). A new language, for example, may
increase their coding efficiency or accuracy -- but, the effort to
become proficient with it is an added (and unknown) "cost".... that the
current project (and deadlines/commitments) will have to bear.

If you have "down time" (and motivation!) between projects, you can
explore new technologies. If, instead, you are moving from one
crunch to the next, you have to decide how much "risk" you want to
add to your current/next undertaking; your boss/client isn't
likely going to "give you credit" for taking on something that
*he* doesn't see as necessary.

> truth? They're afraid the formal analysis will show everyone how wrong they
> are, and have always been.
>
>>>>> I look forward to hearing of your experiences with TLA+, Alloy, or CQL.
>>>>> I promise that it will be worth your effort.
>>>>
>>>> It's unlikely that I will try any of them! This is my last "electronics"
>>>> project (50 years in a field seems like "enough"; time to pursue OTHER
>>>> interests!)
>>>
>>> And that is why I'm sometimes reluctant to engage in these conversations
>>> with you, Don. You're the one asking "why does nobody try this", but even
>>> now you
>>
>> You've misread my intent. I am not ACCUSING anyone. Rather, I am trying to
>> see how people have AVOIDED "doing this". How are folks designing products if
>> they aren't writing specifications, modeling behaviors, quantifying market
>> requirements, etc.? (if they ARE doing those things, then WHICH are they
>> doing??)
>
> Good question. I agree with your thoughts. But that has nothing to do with what
> I was getting at.
>
>>> have time to explore (without the demands of delivering a result), you're
>> Who says I don't have to "deliver a result"?
>>> unwilling to do more than talk about that.
>> Who says I've not "ventured into the uncharted wilderness"?
>
> No-one. Certainly not me. But you've said you're effectively retiring.
> To me that means you don't have to "deliver a result" any more.

I don't have to deliver a result *after* this project -- which I
consider to be my last in this area. But, I'd not have invested
a few hundred kilobucks in something just to piss away time and
money! If I just wanted to "entertain myself", I could watch
a helluvalot of movies for that kind of money!

> But it also means that you can take even more time to explore, if you like to
> go even further from the well-trodden paths, so I suggested a few interesting
> paths that you might like to explore in your dotage. Perhaps learn something
> that you could communicate to help less experienced folk. So I was a bit
> surprised when you said you were unlikely to do that.

For the "risk" reasons outlined above, I see no value (to me) in
taking on yet-another "wilderness" issue. I've added enough
uncertainty to my current effort (have I anticipated every way that
the hardware can be subverted? have I anticipated every way that a
malicious "program" can interfere with benign applications? Have
I chosen components that will STILL be available at the time it all
comes together? Should I have run CAT6 instead of CAT5e? Will
vision technology advance enough to make it more practical in
tracking subjects? ...) So, any additional risk has to yield
tangible short-term reward. E.g., developing the process migration
mechanism gives me an "out" if I find myself in need of more resources
(MIPS/memory) for some particular activity -- just power up another
node and move some of the load onto it!

And, design methodologies aren't likely to be of help to me AFTER
this project (as I want to pursue other interests) so it's an investment
with no LONG-term payoff.

OTOH, if "everyone" was expressing designs in some particular
structured form, then it would have value to THEM (and thus, to me)
if I invested the time to learn enough to be able to translate
my existing designs into such form.

> Instead you blather on about the many things in your past.

I use examples from my past to explain/justify/rationalize
approaches I've used/avoided as well as constraints with
which I've had to live.

I suspect most of my colleagues use THEIR pasts similarly.

None of our FUTURES are known so pointless to "blather on"
about those!

> Guess what? Lots of
> us have many varied experiences in our past. You'd be surprised how widely my
> interests have strayed off the beaten tracks - I'm also a life-long explorer.
> But this is not about me, or about you, it's about how the industries we work
> in could do even better than we could, and what we could yet learn to help them
> do that. I'd still like to add to my legacy, and I hope you would too.

My "legacy" is the products that I've defined and the people I've
influenced. I have no desire to immortalize myself in any of these
things; the *things* are the legacy, not my role in their creation.

E.g., I am hoping that demonstrating how you can approach a (UI) design
differently can eliminate "ability-bias" in the way those interfaces
are designed. I have no desire to go on a "speaking circuit" to
pitch the approach. Few people will actually see/interact with
my end result. But, if it causes them to think A LITTLE about
their UIs, then it will have made a mark (contribution).

> Not just raise a long discussion leading to interesting areas to explore, then
> announce that it was all useless because you don't intend to explore any more.
>
>> All of these are "wilderness" areas. All of them took time to research,
>> implement and evaluate.
>>
>> So, I guess I have a different idea of "having time to explore" than
>> you do!
>
> But that was all in the past. Apparently you no longer have the desire to
> explore. That seems to be what you said anyhow. Correct me if I've misread that:

No, that's all part of *THIS* project. Note the sheer number of "new"
techniques/technologies that I listed. Then, tell me I have no desire to
explore!

The verdict is still out as to how well my redundancy mechanisms will work
IN REAL LIFE. The verdict is still out as to how well my speech synthesizers
will perform when confronted with some yet-to-be-conceived string of
characters. Or, how well my hardware will survive a *real* "attack" -- ditto
for the software. How will my speaker identification software fare when it
encounters someone with a severe case of laryngitis? Or, as those voices
naturally "age"? Will others be able to get the information they need from
the documentation I've prepared?

So, while I have attempted to tackle each of these "wilderness issues",
I still have no idea as to which, if any, will work IN PRACTICE as
well as what the shortcomings of those that miss their mark will likely be.
I'll BEGIN to know that when all of the technologies have been implemented
and deployed. As with any project, those things only are truly understandable
AFTER the project is complete.

In *my* case, that will just be an intellectual exercise as my NEW
activities won't (likely) directly benefit from those past.

> > "It's unlikely that I will try any of them! This is my last
> > "electronics" project (50 years in a field seems like "enough""

Pages:12
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor