Mark's commentary on security issues needs to be made mathematically rigorous

[Carl Hewitt]

Mark's commentary on security issues here

https://docs.google.com/document/d/1cHSXziWOZ_44oSdyaKkJ-X0hTF_OhunIjgnrJ8oycss/edit#

needs to be made mathematically rigorous in order to be 

comprehended by computer systems together with software engineers.

A start on this large project can be found here:

Information Security Requires Strongly-Typed Actors and Theories
       https://papers.ssrn.com/abstract=3418003

Physical Indeterminacy in Digital Computation
        https://papers.ssrn.com/abstract=3459566  

This project has become critical because of the prospective 

development and delployment of Universal Intelligent Systems in this decade.

Regards,

Carl

https://professorhewitt.blogspot.com/

[Christopher Lemmer Webber]

Carl Hewitt writes:

> Mark's commentary on security issues here
>
> https://docs.google.com/document/d/1cHSXziWOZ_44oSdyaKkJ-X0hTF_OhunIjgnrJ8oycss/edit#
>
> needs to be made mathematically rigorous in order to be
> comprehended by computer systems together with software engineers.

A couple of things, in brief:

- I think this article is more aimed at "engineers" than proof-oriented
computer scientists (I know a few people who gain great understanding
just from reading mathematical proofs, but they seem rare). Linking
to papers that bank up the claims Mark is making would be a good
idea, and I believe they exist, but that also might be well served by
a followup article. I'd perceive this paper as a kind of "primer"
document.

- Looking at the links you posted, I know they are positions you
strongly believe Carl, but I don't believe they are the same
positions Mark is posting necessarily (even if there is large
overlap)... so while it might be a good idea to link to articles with
mathematical rigor, they should be the ones analyzing the particular
issues discussed. (Or, again, that could be done in followup
documents... different narrative approaches serve different purposes
for introducing related material.)

Just my $.02, rapidly decreasing in value through inflation!

- Chris

[Mark S. Miller]

If not specifically relevant and understandable, I agree, definitely not in this first Security Taxonomy document. However, this document makes clear that it is to be the first in a series. I would love to see a good formalization that is more obviously relevant and understandable. IOW, I agree with Carl's stated goals, and I'd love to see documents that better satisfy these goals. This would be in addition to the follow up docs I plan to write anyway, none of which I expect to be substantially formal.

Thanks Carl! I hope you and everyone here takes your stated goal as a good challenge. I would love to see something along those lines included in this series.

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/87bldeow1d.fsf%40dustycloud.org.

--

  Cheers,
  --MarkM

[Carl Hewitt]

Thanks Chris!

Proofs themselves need not be read provided that they are correct ;-)

The theory Actors (outlined in the linked articles) is 

the most powerful system available for 

expressing and proving properties of systems, 

particularly highly concurrent ones.

The theory is also the one best defined among existing possibilities because it

characterizes Actors up to a unique isomorphism. 

The important issue is what can be proved?

• Is the theory powerful enough to express properties of systems that need to be proved?
• Is the theory powerful enough to prove properties that have been expressed?

What differences struck you that 

Mark discusses in his article that 

might need to be addressed.

Regards,

Carl

https://professorhewitt.blogspot.com/

PS. I agree with you about the need for many different narrative approaches.

On Sun, Jan 24, 2021 at 1:38 PM Christopher Lemmer Webber <cwe...@dustycloud.org> wrote:

[Carl Hewitt]

Thanks Mark!

We are in the midst of developing and deploying

secure Universal Intelligent Systems (UIS) in this decade.

UIS can become a secure foundation for 

representative government and civil liberties.

However, strong competitors are 

pouring enormous resources into making UIS 

the foundation for totalitarianism and universal surveillance.

Regards,

Carl

https://professorhewitt.blogspot.com/

[Jonathan S. Shapiro]

Carl:

Writing as someone who has done my time in the trenches on formal and rigorous specifications, I am of two minds:

1. It might be good to have a more formal specification, though we both know that correct specification is more elusive than any of us might like, but
2. It's irrelevant for the target audience here, because formal specification is done in a language, style, and framework that is largely alien to this audience of practitioners.

For working engineers, I'd say that the ideal level of rigor today (barring improvements in the comprehensiveness of core CS education that would require more credit hours for a degree) is what the IBM 360 Principles of Operation achieved. While written in English, it is a rigorous and clear specification that was successful in maintaining a compatible processor architecture family over a 30 year period. But equally important, it was written in a language, style, and organization that provided pragmatically relevant and useful guidance to the practitioners.

I'm merely saying that a specification document must speak to its audience if it is to be useful. I think there is an interesting discussion to be had in how that type of writing might be applied to security concerns.

As an aside, my confidence in formal methods was greatly reduced by experience. The problem is that (a) it's too easy to prove the wrong thing, (b) it doesn't scale and it doesn't iterate at reasonable cost, and (c) the set of problems we can successfully apply it to is too specialized, and (d) global pool of people who can do it isn't large enough to be interesting.

All of these issues may, in time, come to be resolved. That said, if our goal is justified confidence, there is a great deal that can be done with various forms of typing that hasn't been adequately explored - or hadn't been when I last did a deep dive on the literature. And yes, that's a kind of formal specification, but one that is expressed in a way that speaks to the practitioners, and one that can often be applied in a "variable weight" way, focusing effort where it is most needed.

With regard to your proposition about Actors, I have two small thoughts and one larger one:

• Some properties require typing, but not all. Notably: systemic information flow properties do not appear to be best addressed by type-based validation.
• We also need open specifications, which is hard to do when the documents suggested as the basis for building them are not publicly accessible. Would you be open to making the documents you have identified more openly available?

With regard to concurrency, the level of abstraction at hand has some influence on the appropriate method. Rather than divert the discussion taking place under this subject, I will post separately.

Jonathan Shapiro

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc0nWE2gqf20%3Dex5vpR72o3dkd_hpN-4OckfVMPVDaRJ7w%40mail.gmail.com.

[Mark S. Miller]

On Tue, Jan 26, 2021 at 1:03 PM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

Carl:

Writing as someone who has done my time in the trenches on formal and rigorous specifications, I am of two minds:

1. It might be good to have a more formal specification, though we both know that correct specification is more elusive than any of us might like, but
2. It's irrelevant for the target audience here, because formal specification is done in a language, style, and framework that is largely alien to this audience of practitioners.

For working engineers, I'd say that the ideal level of rigor today (barring improvements in the comprehensiveness of core CS education that would require more credit hours for a degree) is what the IBM 360 Principles of Operation achieved. While written in English, it is a rigorous and clear specification that was successful in maintaining a compatible processor architecture family over a 30 year period. But equally important, it was written in a language, style, and organization that provided pragmatically relevant and useful guidance to the practitioners.

I'm merely saying that a specification document must speak to its audience if it is to be useful. I think there is an interesting discussion to be had in how that type of writing might be applied to security concerns.

As an aside, my confidence in formal methods was greatly reduced by experience. The problem is that (a) it's too easy to prove the wrong thing, (b) it doesn't scale and it doesn't iterate at reasonable cost, and (c) the set of problems we can successfully apply it to is too specialized, and (d) global pool of people who can do it isn't large enough to be interesting.

All of these issues may, in time, come to be resolved. That said, if our goal is justified confidence, there is a great deal that can be done with various forms of typing that hasn't been adequately explored - or hadn't been when I last did a deep dive on the literature. And yes, that's a kind of formal specification, but one that is expressed in a way that speaks to the practitioners, and one that can often be applied in a "variable weight" way, focusing effort where it is most needed.

With regard to your proposition about Actors, I have two small thoughts and one larger one:

• Some properties require typing, but not all. Notably: systemic information flow properties do not appear to be best addressed by type-based validation.

Hi Jonathan, could you expand on this? That's my intuition as well, but I don't understand it well enough to argue against the common wisdom of the people doing this. Thanks.

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QNYPxvpMGidyDNSZoUvKT2BNBAajr2Jp5nQbTqE%3Dy9j2Q%40mail.gmail.com.

[Carl Hewitt]

Jonathan,

Thanks for your time productively spent in the trenches!

The linked documents in my messages are freely available (not behind a paywall as in other publishers).

Many highly-downloaded articles are published on SSRN.  For example, see the following:

https://papers.ssrn.com/sol3/cf_dev/AbsByAuth.cfm?per_id=2561841

Are you having trouble accessing the articles?

Programmers who are proficient in Java and C++ should be able to deal with formal properties of systems.

Only specialized software engineers need run the proof engines :-)

The IBM 360 voluminous approach will not provide the automation that we need for Universal Intelligent Systems.

Of course, we still need to write articles and documentation in natural language as well ;-)

As you note, formal properties can be as difficult as large software systems to develop and debug. 

Modern Actors are strongly typed (although Mark may disagree).

Also system properties expressed in the theory Actors are strongly typed.

Some information flow properties are expressed 

using strongly-type Actors and Propositions in the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

We are in an Apollo-scale race to develop and deploy 

Universal Intelligent systems by 2030. See the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3428114

The future of representative government and civil liberties 

depends on winning this race.

Regards,

Carl

https://professorhewitt.blogspot.com/

On Tue, Jan 26, 2021 at 1:03 PM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QNYPxvpMGidyDNSZoUvKT2BNBAajr2Jp5nQbTqE%3Dy9j2Q%40mail.gmail.com.

[Bill Frantz]

On 1/26/21 at 4:03 PM, jonathan....@gmail.com (Jonathan S.

Shapiro) wrote:

>As an aside, my confidence in formal methods was greatly reduced by
>experience. The problem is that (a) it's too easy to prove the wrong thing,
>(b) it doesn't scale and it doesn't iterate at reasonable cost, and (c) the
>set of problems we can successfully apply it to is too specialized, and (d)
>global pool of people who can do it isn't large enough to be interesting.

I have watched the IETF TLS working group use formal proofs for
the TLS protocols and much of what Jonathan is concerned about
is quite real. However, the TLS working group avoids much of the problems.

There are a few contributors who have knowlege and experience in
protocol proofs. They apply these skills to the proposed TLS
protocols and report their results. The rest of us accept their
comments, and try to modify the protocols so their proofs work.
This approach allows us to take a protocol that looks to
practitioners to be a good protocol, and get, via a different
route, an assurance that it is good.

So, even if (a) we're proving the wrong thing, it is unlikely to
negatively effect the protocol. We don't apply the proofs until
the protocol is fairly well defined, minimissing the (b) scaling
problems. I think we went through two iterations with TLS 1.3.
(c) and (d) are covered by having experts in protocol proofs who
are interested in TLS because of its importance in the Internet ecosystem.

Think of proofs as, like with types, just another way to look at
a design. The more ways you can look at a design, the higher the
likelihood that it will prove reliable in the field.

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz | There's nothing so clear | Periwinkle
(408)348-7900 | as a design you haven't | 150 Rivermead
Rd #235
www.pwpconsult.com | written down. - Dean Tribble| Peterborough,
NH 03458

[Jonathan S. Shapiro]

On Tue, Jan 26, 2021 at 4:12 PM Mark S. Miller <ma...@agoric.com> wrote:

On Tue, Jan 26, 2021 at 1:03 PM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

With regard to your proposition about Actors, I have two small thoughts and one larger one:

• Some properties require typing, but not all. Notably: systemic information flow properties do not appear to be best addressed by type-based validation.

Hi Jonathan, could you expand on this? That's my intuition as well, but I don't understand it well enough to argue against the common wisdom of the people doing this. Thanks.

I'm not quite sure which part of the long excerpt you included you are asking me to respond to. Let me address this small part first, since I'll be responding to the list regarding formal methods next.

In a very geeky sort of way, I suppose one might argue that all verification is about typing, in the sense that our current understanding of proof stands on a duality between type and proof. But this is more a statement about the mechanics of proof than it is about the nature of the thing being proved. Scott Doerrie did a mechanical verification of confinement using Coq, which is as much about types as it gets. That said, the problem isn't something that is most naturally considered as a problem in types. It's a problem in transitive semi-reflexive graph evolution.

I think my objection here has to do with comprehensibility. Framing the confinement verification as a type-driven exercise makes both the problem statement and the result completely incomprehensible, both as an end result and as a guide to ongoing implementation and evolution. The mechanical verification is good to have, but it's main practical value lies in the fact that Coq is more credible than Butler is. For both implementers and users, it's a lousy framing.

I think there is a huge payoff in ensuring that the "systems" people in CS have a stronger grounding in type theory - notably higher-order type theory. Not as the vehicle for obsession that it sometimes becomes, but as a practical day-to-day reasoning tool.

Jonathan

[Matt Rice]

On Fri, Jan 29, 2021 at 5:38 PM Jonathan S. Shapiro

It's been a while since I watched the following 4 lectures on
Security-Typed languages given by Andrew Myers,
in the first few minutes of it, he argues that strong typing, and
dependent types is not enough "for the notions of correctness" needed
to build secure systems..
Then goes on to add security labels to values confining them within a
lattice, IIRC based on the work on https://www.cs.cornell.edu/jif/

The argument would go I guess that it isn't type-based validation that
isn't helpful for information flow properties,
but that standard types of common type systems don't capture the
problem presented information flow elegantly
in a way that a type-based approach tailored to the problem can.

I think it is fair to admit though there is always going to be
additional cognitive overhead hand in hand with the addition of static
analysis,
But I think he does show that some strong properties can be shown in a
system which I do not think ends up being completely
incomprehensible...

Anyhow it is quite a long series of lectures at some 5+ hours, not
sure if there is a paper version.

https://www.youtube.com/watch?v=9gSY0sRpkbY
https://www.youtube.com/watch?v=jbypDhPJo48
https://www.youtube.com/watch?v=T-4j7r8MVa0
https://www.youtube.com/watch?v=_szMvwq5Cos

[Jonathan S. Shapiro]

Well, Mark asked me to expand; perhaps he will more carefully consider what he asks in the future. :-) Please keep in mind I'm mentally revisiting things I haven't considered in a decade here. There will surely be both omissions and errors.

On Wed, Jan 27, 2021 at 6:42 AM Carl Hewitt <carl.e...@gmail.com> wrote:

Programmers who are proficient in Java and C++ should be able to deal with formal properties of systems.

Only specialized software engineers need run the proof engines :-)

With respect, anyone who has done any significant amount of coding in a substantial, mechanically verified system will tell you that this is not viable. Verification, by its nature, is principally motivated by the need to validate systemic properties; local properties can usually be checked with lighter mechanisms such as static typing. A consequence is that verification is inherently immodular. If you allow significant code changes to accumulate before some specialist brings the verification up to date with the code, the accumulated "verification debt" (by analogy to technical debt) becomes insurmountable from the perspective of ongoing development dollar costs.

On a lighter note, please don't assert this when Gernot Heiser or Gerwin Klein are sitting across from you; you will likely end up wearing their beer. Though in both cases it will be pretty good beer.:-)

That said, I agree with Bill's comment that proofs are just another [very useful] way to look at and validate a design - even when the properties are mis-stated. But we shouldn't fail to note his statement that the non-formal-methodists largely took the word of the formal methodists, and this should be acknowledged as a huge red flag to be addressed over time. And yeah, I know that won't happen overnight. The thing is: if the principal goal is to change the focus of developer attention and the "thought tools" they apply, there are lower cost ways to achieve that goal.

Are formal methodists a doctrinal evolution of insufficiently formal anglicans?

 

The IBM 360 voluminous approach will not provide the automation that we need for Universal Intelligent Systems.

Of course, we still need to write articles and documentation in natural language as well ;-)

By the standards of such things, the 360 spec was not as voluminous as you may think. By the S/370 it had gotten well out of hand, but the S/360 was still something an individual could read and understand in its entirety. Regardless, I identified it mainly as the closest thing we have to a gold standard in such documents. I concur that it does not provide automation, but until we see a qualitative change in what is automatable, that's largely irrelevant. It's a huge step forward from most current practice.

As you note, formal properties can be as difficult as large software systems to develop and debug.

Usually more so.:-) Math is a great way to be precise, but a terrible way to be expressive in human-comprehensible terms on things at this sort of scale.

OK. On to Mark's request. Let's start with two heresies:

Security isn't about confidence. It's about results in the field. Confidence is a sales tool. Security is an objectively measurable and characterizable condition. Both are important, and both are needed, but we shouldn't neglect the second for the first.

The two main thought streams about security concern themselves with (a) confidence and (b) process. What the fuck happened to considerations of (c) structure, and (d) architecture, which are the main things that ultimately determine behavior in the field?

I say this not because I object to confidence - it is a key part of how and why we talk to each other about security issues and methods. Rather, I say it because confidence is not the end goal, and too much of the focus of TCSEC, CC, and their intellectual cousins has set confidence as the finish line.

Which brings me to a third heresy:

Security comes at a cost, and our persistent inability to frame the cost/benefit tradeoff of security-related engineering is part of why the business case for it is so elusive. Without a business case, it simply won't happen.

And yes, I understand that we're on the wrong side of the lever and the need is acute. This doesn't change the fact that verification remains economically impractical at scale even for problems that support it. The fundamental reason for this is the fourth heresy:

Sustainable revenue from software is ultimately driven by on-going change. The majority of software exists in a compulsory feature arms race for economic and business reasons, and the way we have been approaching verification over the last forty years has largely ignored this. There is a fundamental impedance mismatch, and Carl's assertion above about verification specialists seems very close to the heart of it.

Taken collectively, the things that I have said above (including my disagreement with Carl about who does the verification) tell me that verification is not a broadly viable tool for commercial software at this time. To the extent this is true, it's worth reviewing what tools and methods exist that might be commercially viable for a broader class of software. Here are some of my opinions. The first amounts to translating things we already know into practically usable form. The second one is an area where exploratory work might have a large and relatively immediate payoff:

1. Architecture

• I like to think of this as the "Grace Hopper Rule": think in systems. Construct systems from simple components that have well-defined intercommunication and [human comprehensible] semantics and enforced communication channels (the latter so that you know what's going on as they interact). This one is actually very bad, because it turns out we've been evolving the isolation mechanisms in microprocessors in the wrong direction for the last 45 years (hint: protection boundary crossing delays). Worse: Apple just proved that the processor hegemony argument has been completely wrong for just as long.
• We desperately need a strongly typed (in the mathematically formal higher-order sense) systems programming language that admits a checkable allocation-free subset language. I continue to believe that BitC might have been a candidate to fill that niche, but support did not exist that would have allowed me to continue to work on it. We urgently need somebody to pick this problem up.
• We need a way to migrate traditionally-compiled software to safe runtimes. There has actually been enormous progress on this.
• We need to migrate our operating systems to APIs and communication mechanisms that are not insecure-by-design.
• We need to structure systems and components so that they have natural "choke points" where checks can be performed:
• The capability pattern of merging designation with authority induces such choke points pervasively.
• The query "resolver" model in GraphQL, oddly, provides an interesting set of related opportunities (I'll have a whole lot to say on that in six months or so).
• I'm sure that there are others I'm not thinking about. Perhaps we might usefully enumerate more.
• Typescript's limited form of typestate following type guards is quite useful. Enough so to induce structural changes in coding practices (though I might wish for more sophisticated analysis):

// t is nullable<T> prior to this line:

if (t === null) handle_it();

// t is typed as [non-nullable] T from here down

Ultimately, what I'm seeking here is system design patterns that induce the kind of structure on our code and our systems that allows us to bring type checking and "coding to constraints" to bear more effectively.

2. Static Typing

People coming from the C/C++/.Net world often view types as a tool for articulating data layout, and perhaps secondarily as ways of articulating a limited set of object relationships. Over time, I've come to the view that OO as it went into the world has turned out to be one of the most expensive mistakes in software history. Mainly because it's capacity for composition isn't what we actually want and need and the limits it imposes on expressiveness are actively counterproductive. I gather Alan may agree, though I wonder where our thoughts might agree and diverge. If I can get mine cleanly formulated, perhaps I will ask him.

But that said, type systems as they exist go a long way toward stating constraints, and could go much further. I think this is an area we need to focus on. 

• How might we specify something analogous to foreign key constraints? Not merely "this thing must have that type", but "this thing must have that type and be a reference to one of that set of things rather than this set of things". That is: a data level constraint?
• Just now, I'm particularly interested in which foreign key constraints can be composited over union selects; the analogous problem exists for the type-based approach. There are some very modest type annotations that I would really like to see adopted in SQL even if the database cannot enforce them.
• How about static typing for dominance relations? How might we state "this thing can only be touched if that lock is held, or that check has been [witnessably] performed?" Can we come up with typing conventions that combine with code patterns to let us statically validate access checks? I actually believe we can - kernel lock acquisition patterns already do this.
• What about re-visiting Rob and Shaula's work on typestate more broadly, which Typescript is subtly hinting at?
• What about linear typing that isn't unusable due to weak analysis capabilities that are in turn hampered by weak typing?

My point about these is not that any of them solves the security problem. My point is that the security problem (and the pragmatic reliability problem) is often solved by identifying a set of constraints to be maintained and then maintaining them pervasively. In successful systems, most of these constraints are local and structural, are easily, simply, and comprehensibly stated using straightforward typing mechanisms that could be written in the source code, and could be directly checked at compile time if so stated. There are always a few global (systemic) constraints that do not emerge in an "obvious" way from the local constraints - these are the ones that drive us to consider verification. But in successful systems, very few of the essential consistency requirements are global. If we could take a substantial bite out of the local constraint problem by allowing normal programmers (not proof specialists) to specify and enforce the local constraints in the source code (and combining this with type and memory safety), then most of what would be left is the global constraints. My [anecdotally supported] beliefe is that in a system designed to meet constraints one can reason successfully about these remaining global constraints informally. As with verification, designing to constraints qualitatively improves reliability even when the constraints you check are not complete or pervasive. Equally important, this approach is friendlier to code iteration and development than verification is.

At the end of the day, the local structural constraints are 95% of why KeyKOS/EROS/Coyotos actually work. Perhaps more so in Coyotos because we relied on them so heavily to keep concurrency sane. The proof efforts came after the fact. But it would have been a huge help to be able to get better checking on the local constraints as we worked.

3. Introspection-driven Synthesis

I think static typing should be used wherever possible, up to the limits of useful expressiveness (though when it gets too complicated to understand that's a bad sign). I also think that the line between static and dynamic typing is a lot more fluid than has conventionally been true. Typescript's "mapped types" are very thought provoking in this regard, and especially so in combination with union types and its light taste of typestate. Because of the complexity of the types that get generated, type inference is not always as helpful as it might be, and it's a mistake to remove explicitly declared types from a language.

But I'm currently working on a system where the end users add fields to certain data structures in real time, which entails "live" changes to wire protocol, server-side handlers, and the database. All of which is synthesized on the fly, about 85% of which is now working, and the remainder is merely a straightforward slog. In client/server systems, we can't rely on well-formed or well-typed data at the server perimeter anyway; the types are a statement of what we should have received rather than a statement of what we did receive. Validation is necessary. When the APi is fixed, the validator can be built statically. But when the protocol is changing on the fly, the validation must be driven by interpreting metadata derived from some form of type introspection. You can use all manner of run-time code generation and optimization tricks to get that to converge on a direct execution, but you need to be able to replace the code on the fly when fields are added or removed.

Please note that I said "validation". A lot of the higher-order typing community would prefer to get rid of yucky representation details, but to abuse the expression horribly, size does matter. Databases deal in real payloads where overprovisioning has real costs when you go to read records. Whether we think of this as part of types or as field-associated metadata doesn't matter much to me (it depends where and when you want to catch those errors), but we can't ignore it in real systems. Since we aren't in marketing, the rubber needs to meet the road rather than the sky.

Which, in some ways, kind of stinks, because many of the very nice checks I had been getting from using Typescript had to be thrown overboard or severely weakened to do this. It's a huge credit to Anders' work that any of it could remain captured in Typescript types at all.

Incidentally, I think validation, (database) query construction, and API handler construction should probably be synthesized from type introspection and/or metadata in any case. The same tricks I'm using work just fine if the code base is fully statically typed. These things are 100% synthesizable. They are the kind of "code by numbers" stuff that humans are terribly bad at writing consistently, and even worse at maintaining. Ask me over a beer about the very disturbing things that were found when textual self-similarity analysis was applied to the code of the 5-ESS telephone switching system back in the '80s.

At the risk of making an over-stated claim based on incomplete experience, I think this sort of thing is only safe when (a) the schema of the metadata is manageably simple, (b) all of the checks, validations, data marshaling, and queries can be generated automatically from the metadata, and (c) the system is structured to have the kinds of "choke points" that I identified above. So it's pretty clearly a specialized sort of niche, probably in a similar way that allocation-free code is a specialized niche. And there doesn't seem to be much room in the middle between static and fully synthetic if we want reliability and safety. But it's not really a niche we can afford to ignore in a connected world.

Jonathan

[Carl Hewitt]

In order to achieve precision in Foundations, 

types and propositions are intimately interdependent on each other.

Consider the following fundamental Actor Event Induction Axiom, which is 

fundamental to proving properties of digital systems and 

to proving that the theory Actors characterizes digital computation up to a unique isomorphism thereby removing all ambiguity:

∀[P:Sentenceviw^EventvSw]                         // For every predicate P of order i on events of S,

   (∀[e:FromOutside vSw] P[e]                          // if P holds for every event from outside S

      ⋀ ∀[e:Event vSw,                                                 // and for every event of S

              f:ImmediatelyFollows vew]                // and for every f immediately following e

                   P[e]⇒P[f])                                                // if P holds for the e, then P holds for f

         ⇒ ∀[e:Event vSw] P[e]                            // then P holds for every event of S

In the Event Induction Axiom, in addition to all the other strongly typed variables,

the predicate P is strongly typed to be of type Sentenceviw^EventvSw.

Regards,

Carl

https://professorhewitt.blogspot.com/

[Carl Hewitt]

[Hewitt and Baker 1977] may have been the first to begin characterizing Actor address information transfer among different computers in "Laws of Locality".

Proving confinement with a Citadel is as much about propositions as it is about types.

Address Information Transfer Axiom 

       ∀[P:Propositionviw^Addresses ]                                                                                  // For every predicate P on addresses of propositions

        (∀[e:FromOutside vSw] P[AddressInfo[e]]                                // if P holds for the address info of every event from outside S

           ⋀ ∀[x:ActorvSw] 

                   x:Primordial ⇒ P[AddressInfo[Creation[x]]]                         // and if x is primordial, P holds for the address info in the creation event of x

              ⋀ ∀[e:Reception vxw, e₁:Scoped _Svew] P[AddressInfo[e]]⇒P[AddressInfo[e₁]])

                                                                                        // and if for every reception e of x, if P holds for the address info of e, then P holds for

                                                                                           // the address info of every event of  in the region of S in mutual exclusion of e

        ⇒ ∀[e:EventvSw] P[AddressInfo[e]] // then P holds for the address info of every event of S

In the theory Actors, the following can be proved

    Theorem.  ∀[e₁:Event, e₂:Event ] e₁↝e₂ ⇒ AddressInfo[e₁]⊑AddressInfo[e₂]

Regards,

Carl

https://professorhewitt.blogspot.com/

PS.  I agree with Jonathan that there is a huge payoff in 

ensuring that the "systems" people in CS have a stronger grounding in using types.

[Carl Hewitt]

Without automation, we are going to have tremendous problems 

developing and deploying Universal Intelligent Systems in this decade.

This automation will involve rigorously specify both local and nonlocal properties.

Of course, specifying properties must go hand-in-hand with developing implementations ;-)

Cheers,

Carl

https://professorhewitt.blogspot.com/

[Mark S. Miller]

On Sat, Jan 30, 2021 at 3:39 PM Carl Hewitt <carl.e...@gmail.com> wrote:

[Hewitt and Baker 1977] may have been the first to begin characterizing Actor address information transfer among different computers in "Laws of Locality".

Hewitt and Baker 1977 is one of my all time favorite papers in CS. However, ain't no types in that paper.

 

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc2qTYcFYPRC2Tutm7%2BAqK-W%3Dz6oW%2B3-POfBPUyhYYQ68A%40mail.gmail.com.

--

  Cheers,
  --MarkM

[Carl Hewitt]

PS.  Even if Jonathan is correct that we can't deal with formal properties,

there is an aggressive competitor highly motivated to master formal properties!

[Carl Hewitt]

Thanks Mark for your appreciation of "Laws of Locality" over all these years!

Although type Actors were not well understood in the the early 1970's, 

the following were clearly understood:

• piecing together an Actor address does not require knowing the type of the address
• a type is an Actor because of the fundamental thesis that "Everything is an Actor."

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjEYXDOscf9b%3D2YVMR0GnVMaFscknUA76-ubGzZO_K8EQ%40mail.gmail.com.

[mostawe...@gmail.com]

"Everything is an actor" implies that there is a category of actors. We can sketch such a category briefly.

First, let's consider object graphs as categories. Let the objects of the category be the vertices, the objects themselves; and let the arrows be the paths from one vertex to another along connected edges. When an object has multiple paths to another object, we may distinguish the corresponding arrows. For a given object graph G, call the corresponding category Path(G) (sometimes called the "path category" or "category of paths of G"). Then our standard flavor of isolation is:

In Path(G), an object B is isolated from A just in the case where there are no arrows A -> B.

Doing a bit of basic abstract nonsense, elements of objects A would be ways to start with a reference to the terminal object, which should be trivial, and then building the target object from nothing. These would usually be literal values. Generalized elements A -> B are the potential ability for A to invoke B under some certain conditions.

We can put functors between these categories to simulate the evolution of heaps over time. Imagine heap mutations as functors. To connect one object graph G to another G`, as in the E literature (e.g. MarkM's thesis), we construct a new family of arrows for the new paths in the graph, but these arrows can't be addressed functorially; these paths really are new and don't exist in G. The functor itself is the only way to designate this family, since its image is G and G does not have them. So functors into Path(G) can name the introductions between subgraphs. I am handwaving, but I think that the only other functorial heap mutations are GC actions, where we represent the GC's reaped objects as a single special reaped reference and change Path(G) into Path(G) + 1. In general, a functor F : G -> G' can't fail to use a path; if A can address B in Path(G) along f : A -> B, then A can also address B in Path(G') with the arrow F(f) : F(A) -> F(B). So:

Functors into Path(G) are precisely the introductions between subgraphs; functors into Path(G) + 1 are either (factorizeable into) such introductions, or are GC actions.

We're almost there! What is an actor, but a miserable pile of object references? Well, I guess it's also got a script. The script allows for the actor to be invoked, and an invocation involves the actor becoming a new pile of object references, by a series of action rounds. In each action round, the references are permuted, and then a recursive invocation is made. Crucially, the number of rounds is static and fixed (each script is finite) but the object graph need not be acyclic and so recursion can diverge. Assuming it terminates, then the actor will have a new collection of references, including possibly new references passed along during invocation, and also it may have caused other effects although we'll formally just consider the effect of having caused other actors to also update their collections. We'll also allow actors to forget references, if they really want to.

So, now, an actor formally has a script which contains a sequence of functors. Each functor rolls in the permutation (since it just relabels the actor's internal collection) and then performs heap mutations and invocations. Heap mutations have been explained already. When an invocation occurs, we need to account for divergent recursion, and this means that we need to cut our semantics into smaller steps. In particular, let's insist that the functors themselves are somewhere in a bigger object graph where the actor itself is an object! Then, we could use standard internal-hom technology to load functors from actors without circularity or infinitely long compositions.

(On proofread, I realize that I should explain this connection formally in more detail. An actor stores a labelling S on some object graph G along with G itself, and its script is a functor S -> (Path(G) + 1 -o Path(G`) + 1) which picks out a functor to do the dirty work on the heap. The actor has a bird's-eye view and can choose to save references from G` for its storage; the actor is allowed to update its labelling S. The upshot is that the actor really does have full control over its private storage, even though it seems like it only has control over its root references.)

Let's call this bigger category Act. The objects of Act are actors as mentioned, and the arrows are still the isolated ability to invoke, but now each actor can maintain a private heap where it manages its own isolated store of references. By fiat, there's an actor with an empty script and an empty private collection, and by a bit of exercise-for-the-reader, this is Act's terminal object. (e`null` or m`null` perhaps, but more like objc`nil`!) By more fiat, we can imagine an actor who takes three references, semidecides some property of the first reference, and returns either the second or third reference appropriately, and this actor will serve as our subobject classifier. Thus Act is Cartesian closed and a topos, and more folklore is proven:

Act has an internal lambda calculus with the isolation property. All lambda calculi whose topoi have logical functors out of Act (that is, that are at least as rich as Act) also have the isolation property.

It might worry the reader that Act's arrows are not total. But this suggests to me that Act should be a Turing category, where the partiality of arrows is balanced by access to the full power of Turing-complete computation. A Turing category requires at least one object, the Turing or Gödel-numbering object, whose elements are code literals; and two partial families of arrows for sending values into and out of said Turing object. Assuming such functionality is available, then a variety of handwaves will bring us Kleene's Recursion Theorem and then we are free to program as we normally would.

I kind of assume that message delivery is reliable and exactly-once; anything remote here would behave like synchronous RPC and be horrible ergonomically. That is, Act really only models the programming on a single-core local CPU-bound process with unlimited RAM, as is our tradition. An asynchronous Act can be produced by allowing the partiality of Act's arrows to not be due (only) to Turing issues, but also due to network failure or etc. Note that the isolation theorem lifts for free without any effort, and it should hopefully have the same shape in your imagination as MarkM's original argument on graphs.

Finally, on types, three things. First, category theory is typed; objects serve as types. Second, Turing categories are unityped; each Turing object serves as a stand-in for all other objects, and partiality is like stuckness of wrongly-typed programs. Third, to quote Malaclypse the Younger, "I don't know, man; I didn't do it;" I'm not responsible for this paradox's existence, only for highlighting it here.

Sorry if I'm sounding like Mojo Jojo and repeating myself here. I feel like I've said most of this before, but I also feel like this is the first time that I've said it and it feels like I've actually proven all of the important bits to myself. The bad part is that we didn't learn much that's new, but the good part is that the proofs were easy.

Peace,

~ C.

[Carl Hewitt]

The key theorem to be proved is that there is a unique model for Actors up to a unique isomorphism as done here:

Physical Indeterminacy in Digital Computation

        https://papers.ssrn.com/abstract=3459566

The only way known to prove the unique isomorphism is to the the full Actor Event Induction Axiom.

Cheers,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/0358607b-ef70-4e56-a9b6-662db364c3e2n%40googlegroups.com.

[mostawe...@gmail.com]

There cannot be a single unique model up to unique isomorphism for *any* Turing-complete computational system, if the following sketched object exists.

Let each computational system have a Turing category in the standard way, and also let them (WLOG) have natural numbers objects (NNO). Crucially note that Turing categories do not have to have a unique Turing object up to isomorphism; there can be multiple Turing objects and the adjunctions between the Turing objects exist but need not be isomorphic and certainly need not be unique. This is the key feature which blocks your desire.

(Why is it legal to assume NNO WLOG? Because non-trivial Turing categories have to have at least an infinite number of elements in their Turing objects, and so if there's no other NNOs, usually a Turing object can be abused to do the job.)

Note that it is possible to translate one Turing category to another. We can take the code literals of one language, use the NNO to turn them into natural numbers, send the natural numbers to another category, and recode them to new code literals in the new category. These are compilers! And it is possible for compilers to be computable; in fact, because we're only using Turing arrows and natural numbers, we have them computable from basic appeal to Kleene's Recursion. So, within a single Turing category, we find compilers which allow that category to be remapped to any other Turing category. There's no one single model for this, but instead it shows that Turing-equivalence of all of the different models of Turing-complete computation.

There is a unique object here but it's big. Treat a compiler as a functor which sends an entire Turing category (through one of its Turing objects) to another Turing category. When functors are ordinary objects like this, we obtain an ∞-category whose objects are Turing-complete computational systems, whose arrows are compilers, whose 2-arrows are compiler compilers, and so on. I call this object Tomb, after "tombstone diagram", but there might be other names for it already. Tomb surely has only one unique model up to unique isomorphism, since its models are universal Turing machines, but only if we ignore runtime constants and focus on Halting.

Peace,

~ C.

[Carl Hewitt]

The following article proves that some very simple digital computations cannot be performed by a nondeterninistic Turing Machine:

• Vanquishing ‘Monsters’ in Foundations of Computer Science: Euclid, Dedekind, Russell, Gödel, Wittgenstein, Church, and Turing didn't get them all ...

                https://papers.ssrn.com/abstract=3603021

Regards,

Carl

https://professorhewitt.blogspot.com

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/36bd675f-7c4b-44f8-b929-6e6a853eb560n%40googlegroups.com.

[Carl Hewitt]

Mostawe:  Can you find any bugs in the proof of unique isomorphism in the following:

Physical Indeterminacy in Digital Computation

        https://papers.ssrn.com/abstract=3459566

Regards,

Carl

https://professorhewitt.blogspot.com/

---------- Forwarded message ---------
From: Carl Hewitt <carl.e...@gmail.com>

[Bill Frantz]

On 1/29/21 at 3:46 PM, jonathan....@gmail.com (Jonathan S.

Shapiro) wrote:

>By the standards of such things, the 360 spec was not as voluminous as you
>may think. By the S/370 it had gotten well out of hand, but the S/360 was
>still something an individual could read and understand in its entirety.
>Regardless, I identified it mainly as the closest thing we have to a gold
>standard in such documents. I concur that it does not provide automation,
>but until we see a qualitative change in what is automatable, that's

>largely irrelevant. It's a *huge* step forward from most current practice.

Well, I think that Norm and Charlie understood the S/370
Principals of Operation. (I also think that I understood it as
well, but I might be overly optimistic.)

Learning to appreciate the subtleties takes more than one
reading, and sometimes the experience of having them bite you as
you code.

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz | Can't fix stupid, but | Periwinkle
(408)348-7900 | duct tape can muffle the| 150 Rivermead
Road #235
www.pwpconsult.com | sound... - Bill Liebman | Peterborough, NY 03458

[mostawe...@gmail.com]

Hm. To ask an implicit question, is it really possible to send two messages concurrently to an actor so that one of those messages might be indefinitely delayed, but both messages will both be delivered for sure eventually? The usage of "concurrently" and "faster" makes me curious about the actual physical difficulties of constructing Actor machines. For comparison, the complexity class BQP gives us pretty strong rules about what we can and cannot do with quantum computers; the theory does not extend into the supernatural or unconstructible.

Another problem which makes it difficult to get off the ground is the combination of products and exponential objects. Any such category risks becoming Cartesian closed, but even before that, we must decide which flavor of function is the one which corresponds to exponential objects. This is because, for any types X, Y, and Z, there's an isomorphism between functions like f: (X ,Y) -> Z and f_curried : X -> (Z**Y). What are the consequences? We basically have to choose whether partial functions or total functions will be the basis of our type theory. The axioms given suggest that total functions are the builtin ones. (There's another few ways to do it, but we'll always end up with the total functions being a subcategory of the partial functions.)

We'll have to use computability to approach a model of partiality, but this would turn any NNO into a Turing object, and then we've got a Turing category again. This would make your construction simply a particular diagram with particular objects Actor and Event, and particular arrows Release : (Actor, Event) -> Event and Acquire : (Actor, Event) -> Event, and particular 2-arrows [Release; Acquire] => [id] : Event -> Event, and etc.

If we are Cartesian closed at all, then Lawvere's fixed-point theorem manifests. This monster of a statement (http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf although Yanofsky's https://arxiv.org/abs/math/0305282 is much easier!) says that, in any Cartesian closed category, we have a variant of Cantor/Gódel/Turing/Tarski's main statement, an essential incompleteness wherein the theory cannot prove certain kinds of self-referential statements. I think that this can be sharpened, but a brief summary would be that the claims of escaping the Church-Turing limitations on computability and Gödel limitations on self-reference are unsupportable, as the type theory already has all of the categorical properties necessary for Lawvere's theorem to be summoned.

Typically, a proof which picks out a (Dedekind-)categorical structure, a second-order structure which is identified by set-theoretic properties, will say, "for types T,U,V,..., arrows f : T -> T, g : T -> U, ..., ..., there exists some particular unique arrow u which makes the following diagram commute". WP and nLab have great example proofs for the natural numbers objects:

* https://en.wikipedia.org/wiki/Natural_numbers_object

* https://ncatlab.org/nlab/show/natural+numbers+object

The traditional proofs with second-order logic statements are hard to read, but the comments show the shape of the argument well enough, and I think that it could be formalized into a categorical diagram. The bugs are all in the arguments which lead up to the proof statement.

I alluded to it in the opening, but I think a better path forward would be to define a new complexity class, Polynomial Actors or PA for short (please don't let this be the name, please somebody choose a better name) which is like P but for Actor computation. Given a linear/quadratic/etc. number of events, how much work can get done with Actors? Is it more than with Turing machines, which is how P is typically defined, or with quantum computers, like how BQP is defined? The existing comparison with NP would then be reusable as a demonstration that P vs PA is a meaningful and interesting question regardless of how P vs NP is settled.

[William ML Leslie]

On Tue, 2 Feb 2021 at 14:56, mostawe...@gmail.com <mostawe...@gmail.com> wrote:

I alluded to it in the opening, but I think a better path forward would be to define a new complexity class, Polynomial Actors or PA for short (please don't let this be the name, please somebody choose a better name) which is like P but for Actor computation. Given a linear/quadratic/etc. number of events, how much work can get done with Actors? Is it more than with Turing machines, which is how P is typically defined, or with quantum computers, like how BQP is defined? The existing comparison with NP would then be reusable as a demonstration that P vs PA is a meaningful and interesting question regardless of how P vs NP is settled.

+1, Bounding by the number of events is a great idea.  My primary objection to the Reals example is usually that, in order for it not to be a boring turing-representable stream/codata example, there needs to be an infinite number of actors to represent the places, and that such a construction is not a meaningful model of computation we can actually perform.  Phrasing it in terms of the number of events makes the distinction clearer.  If it takes an infinite number of events to distinguish two real number actors, in what way is their distinction meaningful?

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/ccc3209a-b29b-457f-a79c-48c1632a803an%40googlegroups.com.

--

William Leslie

Q: What is your boss's password?

A: "Authentication", clearly

Notice:
Likely much of this email is, by the nature of copyright, covered under copyright law.  You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in.  Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.

[Alan Karp]

mostawe...@gmail.com <mostawe...@gmail.com> wrote:

Hm. To ask an implicit question, is it really possible to send two messages concurrently to an actor so that one of those messages might be indefinitely delayed, but both messages will both be delivered for sure eventually? The usage of "concurrently" and "faster" makes me curious about the actual physical difficulties of constructing Actor machines.

As someone who is currently working on computer networks, I can say that it is possible, but engineers have very different definitions of "indefinitely" and "eventually" than theoreticians.  Even worse, you can send one message after another, and the second can reach its destination before the first.  Analysis should be easier with synchronous, in-order networks.

--------------
Alan Karp

[Carl Hewitt]

PS.  I would be a very serious limitation, if category theory cannot 

characterize Actors up to a unique isomorphism.

[Carl Hewitt]

The Internet could be modeled to the effect that two 

packets could be concurrently sent to 

another node so that one packet is 

received an indefinite time after the first packet is received.

Also, for reasons of performance and robustness, it is 

possible for one packet to be sent and another packet to be sent, but 

have them received in the other order.

Do you think that TCP-like protocols should 

be the only ones used on the Internet.

For Actor systems in large-scale Intelligent Applications restricted 

to using TCP-like protocols the following hold:

• The performance limitations  are even more severe
•  System understanding is made more complicated

Regards,

Carl

https://professorhewitt.blogspot.com/

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z1jeoBC_XgpGTBj6HQ8r7jZ%2BzwSMG3LZum%2B6aY6zpBS5A%40mail.gmail.com.

[Carl Hewitt]

PS. If a dependency is required that another Actor has received a message M, 

often a better bet is to first receive a response that the other Actor has received M. 

[Ben Laurie]

On Tue, 2 Feb 2021 at 11:23, Carl Hewitt <carl.e...@gmail.com> wrote:

PS. If a dependency is required that another Actor has received a message M, 

often a better bet is to first receive a response that the other Actor has received M.

https://en.wikipedia.org/wiki/Two_Generals%27_Problem

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc0aaByUztb-esbVeu1Hm_LXFtOF9X7DPV00vxeudpktgQ%40mail.gmail.com.

[Carl Hewitt]

Thanks Ben!

It is relatively easy to formulate requirements that cannot be implemented :-(

The real world must deal with actual conditions.

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9SSpt1m5uf8i3EUT9xK%2BRVmmp0KMELeYy0hujQNMS%2BV3Pw%40mail.gmail.com.

[Bill Frantz]

On 2/2/21 at 8:15 AM, cap-...@googlegroups.com ('Ben Laurie'
via cap-talk) wrote:

>
>https://en.wikipedia.org/wiki/Two_Generals%27_Problem
>

An example that frequently occurs in my life is in ham radio
contesting. Contests are judged by comparing the logs of all the
stations. If a contact is in both logs, and the required
information (called the exchange) is correctly transmitted, then
both stations get credit for the contact. If the exchange is
wrong in one of the logs, than that station loses credit, but
the other one, with the exchange, gets credited.

The 2 generals case is when the contact is on one log but not in
the other. This is called a Not In Log (NIL) situation. One way
this can occur is if station A thinks the contact was completed,
but station B does not.

Normally having there are good reasons to think the other
station is logging the contact. Station A sends her exchange.
Station B responds with his exchange. If B receives a "thank
you" (TU in morse code), then he knows that A received his
exchange and A knows that B received her exchange because he
sent his. Both stations log the contact.

If the the TU gets lost then the B is in a 2 generals situation,
but there are still reasons to assume that A received B's
exchange. If A immediately goes on to ask for contacts from
other stations, then B can assume the TU got lost and logs the contact.

It is interesting that there are a lot more NILs in certain
digital modes than there are in either morse code or voice
contacts. These modes are largely automated, and the automation
does not give the additional clues we can get with Morse code or voice.

Cheers - Bill

----------------------------------------------------
Bill Frantz | Art is how we decorate space,
408-348-7900 | music is how we decorate time.
www.pwpconsult.com | -Jean-Michel Basquiat

[Carl Hewitt]

Bill, thanks for the interesting analog case!

In the case of digital systems, a message received can 

be required to be signed and dated by the sender.

Cheers,

Carl

https://professorhewitt.blogspot.com/

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/r480Ps-10146i-CE7663DF9E324D829A2F40A2F1D4EDF0%40Williams-MacBook-Pro.local.

[Alan Karp]

Carl Hewitt <carl.e...@gmail.com> wrote:

PS. If a dependency is required that another Actor has received a message M, 

often a better bet is to first receive a response that the other Actor has received M. 

Halpern and Moses showed that may not be sufficient.  The sender of the acknowledgement may need to know that it was received.  In fact, there are cases, e.g., the general's problem, that require an infinite number of messages.

--------------
Alan Karp

[Carl Hewitt]

Of course, the specification in the General's story cannot be implemented.

If it is desired to know if an Actor has received a message marked uniquely,

just keep sending the message until notified that it has been received ;-)

Maybe the Actor is no longer operational and will never again be operational.

In order to know if an Actor has received a notification receipt,

then the Actor should be queried to that effect.

Cheers,

Carl

https://professorhewitt.blogspot.com/

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z1Cx_UCWJNGAuzJ-YvFz6xLFN-AUxq9TJo6%3DCTRwhx%3Dpg%40mail.gmail.com.

[Alan Karp]

The general's problem is about coordinated action and is unimplementable.  There are other problems that require lesser degrees of common knowledge that are.  

Say that you have a piece of work that you want done exactly once.  That goal can be achieved with 1 1/2 round trips (2 if you don't want the initial sender to be permanently blocked), what Halpern and Moses call E1 common knowledge.

--------------
Alan Karp

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc0y%2Btn-s4goeHTXj8-YkK82M%2Bn%3D-CnXEhHfYZ96gC9C3g%40mail.gmail.com.

[Jonathan S. Shapiro]

On Sun, Jan 31, 2021 at 3:56 AM Carl Hewitt <carl.e...@gmail.com> wrote:

PS.  Even if Jonathan is correct that we can't deal with formal properties...

That's not quite what I said, but it is accurate enough for now. I think everybody here has read about just how many iterations it took to arrive at a correct formal specification for something as simple as a sort algorithm. That specification problem hasn't gotten substantially easier in modern mechanized provers.

Because they are generally graph properties, the specification of information flow objectives is actually easier than the specification of sort algorithms. Even so, it isn't unknown to arrive at a correct formal capture of a mis-stated property. From memory, the originally published seL4 isolation verification inadvertently did this. I'd have to go back to the paper and re-read, but my memory is that they arrived at a correct formalization of a slightly incorrect goal statement on that very early work. What's remarkable is not that a mistake may have been made, but that the mistake (again from memory) was in the original informal statement of the desired property, and none of the reviewers caught it. Because it was a "plain language" issue, the humans had a pretty good chance of noticing the problem. Had it been an omission in the formal maths, the likelihood of catching it would have been so close to zero as makes no difference. And it wasn't the type of error that is readily caught in the course of the verification. Verification often can be used as a co-validation of the refinement of the goal specification, and it can sometimes discover contradictions in the goal statement, but it does not diagnose omissions or errors in the goal statement.

The justifiable confidence achieved from formal verification is the weaker of the verification itself and the specification. We know that the verification efforts are difficult, but more critically, we know that creating the specifications is an activity with a very high error rate. And that's just for simple properties. End-to-end correctness properties are anything but simple.

It is appropriate to ask "How can we improve the specification process?" and I expect that will be an open, long-term research process. But it is also reasonable to ask "Can the confidence we are actually getting be had with a simpler mechanism that can be used by a broader audience, e.g. slightly stronger typing combined with rigorous (but not mechanized) argument?" I currently believe that (for now) the answer is "yes".

This is not, by the way, an argument about the expense of verification. It's pretty well documented that the reduction in error/bug rate that comes from verification is a significant win over the long haul. Dependent type systems can be pushed a good ways into that, but the complexity of a dependent type has a way of exploding quickly when it is pushed in this sort of way.

Unfortunately, there is a serious cost to verification: time to market. While verification yields more robust results, it also tends to drive longer delivery cycles. In the market, it is frequently the case that arriving first, even with a weaker offering, provides market victory. In my view, this remains an open problem to be solved for verification to become mainstream. In essence: the process needs to be much more incremental.

Jonathan

[Carl Hewitt]

Thanks for your incisive remarks, Jonathan!

The main power may derive from the interplay between formal system properties and implementations.

I agree that formal system properties are just as much subject to bugs as implementations.

Also, omitting an important property can have serious consequences.

There is significant value in having formal properties even if they cannot be proved.

Strong parameterized types are in relatively good shape and 

can even be used in modular proofs, such as the following:

Physical Indeterminacy in Digital Computation

        https://papers.ssrn.com/abstract=3459566

The time-to-market issue can be addressed by co-developing implementations with their formal specifications.

Regards,

Carl

https://professorhewitt.blogspot.com/

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMV2N2cMkQto%2BpViH8vbZ6ijvjA2SQ0X6Ev5VX0FnwKiA%40mail.gmail.com.

[Mark S. Miller]

On Tue, Feb 2, 2021 at 10:49 AM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

On Sun, Jan 31, 2021 at 3:56 AM Carl Hewitt <carl.e...@gmail.com> wrote:

PS.  Even if Jonathan is correct that we can't deal with formal properties...

That's not quite what I said, but it is accurate enough for now. I think everybody here has read about just how many iterations it took to arrive at a correct formal specification for something as simple as a sort algorithm. That specification problem hasn't gotten substantially easier in modern mechanized provers.

I have not seen that one. Do you have a link?

 

Because they are generally graph properties, the specification of information flow objectives is actually easier than the specification of sort algorithms. Even so, it isn't unknown to arrive at a correct formal capture of a mis-stated property. From memory, the originally published seL4 isolation verification inadvertently did this. I'd have to go back to the paper and re-read, but my memory is that they arrived at a correct formalization of a slightly incorrect goal statement on that very early work. What's remarkable is not that a mistake may have been made, but that the mistake (again from memory) was in the original informal statement of the desired property, and none of the reviewers caught it. Because it was a "plain language" issue, the humans had a pretty good chance of noticing the problem. Had it been an omission in the formal maths, the likelihood of catching it would have been so close to zero as makes no difference. And it wasn't the type of error that is readily caught in the course of the verification. Verification often can be used as a co-validation of the refinement of the goal specification, and it can sometimes discover contradictions in the goal statement, but it does not diagnose omissions or errors in the goal statement.

The justifiable confidence achieved from formal verification is the weaker of the verification itself and the specification. We know that the verification efforts are difficult, but more critically, we know that creating the specifications is an activity with a very high error rate. And that's just for simple properties. End-to-end correctness properties are anything but simple.

It is appropriate to ask "How can we improve the specification process?" and I expect that will be an open, long-term research process. But it is also reasonable to ask "Can the confidence we are actually getting be had with a simpler mechanism that can be used by a broader audience, e.g. slightly stronger typing combined with rigorous (but not mechanized) argument?" I currently believe that (for now) the answer is "yes".

This is not, by the way, an argument about the expense of verification. It's pretty well documented that the reduction in error/bug rate that comes from verification is a significant win over the long haul. Dependent type systems can be pushed a good ways into that, but the complexity of a dependent type has a way of exploding quickly when it is pushed in this sort of way.

Unfortunately, there is a serious cost to verification: time to market. While verification yields more robust results, it also tends to drive longer delivery cycles. In the market, it is frequently the case that arriving first, even with a weaker offering, provides market victory. In my view, this remains an open problem to be solved for verification to become mainstream. In essence: the process needs to be much more incremental.

Jonathan

[Bill Frantz]

I think message authentication is probably good enough given the
environment. We have a contest where to score points you need
the active cooperation of your opponent. People can be
recognized by their voices, their Morse keying, and their
specific messages.

There are exceptions. Sometimes when conditions are really bad,
and several stations are using the same frequency, a response
from one station can be logged as coming from another station.
Then there are band conditions. I remember in one contest
hearing two stations asking for callers on the same frequency,
alternating time slots. They didn't know each other was using
that frequency since they were in each others skip zones. I
managed to work both of them. :-)

Cheers - Bill

On 2/2/21 at 10:39 AM, carl.e...@gmail.com (Carl Hewitt) wrote:

>Bill, thanks for the interesting analog case!
>
>In the case of digital systems, a message received can
>be required to be signed and dated by the sender.
>
>Cheers,
>Carl

>*https://professorhewitt.blogspot.com/*

[Jonathan S. Shapiro]

On Tue, Feb 2, 2021 at 11:04 AM Carl Hewitt <carl.e...@gmail.com> wrote:

The time-to-market issue can be addressed by co-developing implementations with their formal specifications.

I think you're in the wrong order of magnitude by several orders, but perhaps I am not up to date. Can you identify any example of a substantial application program and associated verification system in which a critical bug can be successfully fixed and verified with 24 hour turnaround time?

We can certainly do this with strong typing, and in comparison to the current state of verification it does not seem clear (at least to me) that the justified confidence from that process is any less than the justified confidence that emerges from current verification processes.

Key questions here (which have no simple answer) include:

• Did the verification answer the right question?
• What justified confidence is obtained from simultaneous checking of multiple properties that may individually be less comprehensive? I've never seen any attempt to quantify this objectively!
• What are the relative labor costs of the verification team vs. the QA team during initial development? Even if we accept as an axiom that the total lifetime cost of the system is improved, project funding is determined by the capital cost to develop and the delay to break-even.

I'm not setting this out to be depressing or to knock verification. I think it's entirely possible that these things are converging and will continue to do so, and I think continued research progress is important.

But the case for verification becoming the standard of practice is ultimately a business case, not a technical one. To the extent that this is true, it's important to recognize that lifetime cost reductions won't win the argument if upfront capital costs and time to break even take longer.

The way to think about a venture investment is that it's a loan you have to pay off at a compounded interest rate of 35%. Every day it takes to get to break even is more expensive than the previous day and the longer it takes the bigger the increase gets from one day to the next. In practice, this means that time and cost to market is actually more important than total lifecycle cost.

At least, this was true before the era of pump-and-dump IPOs (err, umm, I mean Unicorns). Nowadays, concrete revenue prior to public offering means that your fanciful IPO story can be concretely tested. I think it's fair to say that this creates perverse incentives...

Jonathan

[Alan Karp]

Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

On Tue, Feb 2, 2021 at 11:04 AM Carl Hewitt <carl.e...@gmail.com> wrote:

The time-to-market issue can be addressed by co-developing implementations with their formal specifications.

I think you're in the wrong order of magnitude by several orders, 

I agree for products in general, but what about key libraries, particularly widely used open source projects?  I can imagine the effort would pay off for everyone.  Of course, there's still the question of who would pay for it.

--------------
Alan Karp

[Jonathan S. Shapiro]

On Tue, Feb 2, 2021 at 11:07 AM Mark S. Miller <ma...@agoric.com> wrote:

On Tue, Feb 2, 2021 at 10:49 AM Jonathan S. Shapiro <jonathan....@gmail.com> wrote:

I think everybody here has read about just how many iterations it took to arrive at a correct formal specification for something as simple as a sort algorithm. That specification problem hasn't gotten substantially easier in modern mechanized provers.

I have not seen that one. Do you have a link?

Peter Gutmann's dissertation provides a quality dose of rigorously sourced cold water regarding verification. Chapter 4 is not recommended for anyone who (a) favors verification, and (b) has the slightest susceptibility to depression.

The book based on the dissertation is significantly expanded, notably including the subject matter of that chapter.

Peter supports verification as an approach; it's what his dissertation is about. But he also feels that the perils and pitfalls need to be addressed openly.

Jonathan

[Jonathan S. Shapiro]

Since general purpose systems largely defy informal specification (never mind formal specification), I think the scope of the current discussion is probably limited to tightly scoped fixed-function systems, inductive algebraic systems, and some types of protocols.

My understanding of the state of the art is now a decade stale, but at that time the sweet spot for systems verification was systems with fixed external specifications (feature creep and verification don't mix) and fixed finite resource bounds per instance (though those can be parameterized). If those two constraints both hold, you're essentially dealing with a (potentially very large) state machine. Assuming the property of interest actually holds, you're well within the bounds of feasible mechanized verification provided you have adequate compute resources and a suitably talented verification team.

The people who build this class of system are largely systems people. The overlap between this group and people who understand higher-order logic and/or dependent type systems (which lie at the heart of modern provers) is... small. There's my former group, Gernot's group, some of Hermann's group, some graduates of Frank Pfenning's group, and the group that (literally) saved Mercedes from bankruptcy. There's a group at the Advanced Physics Laboratory that does heavily classified things, and there are comparable teams in Europe. I'm sure there are other commercial teams I don't know about or have forgotten about. But if you're looking at the intersection of these skill sets, I doubt very much that the total world supply of candidates reaches 150 souls. Given which, the fact that they aren't high-value hires really tells you something about how their work is perceived. At one point there was a fairly good group at NSA, but it appears that they lost the internal resource battle to the crypto nitwits who brought us such successes as Clipper and its friends.

No offense to Carl intended or implied by excluding him; I simply don't happen to know how his group's efforts are focused, and I'd appreciate learning.

Jonathan

[Alan Karp]

I was talking about applying formal methods to things like OpenSSL.  The leverage you'd gain is probably worth the cost if only someone would pay for it.

A few years back, I attended a celebration of John Mitchell's 60th birthday.  One of the talks described the formal verification of a helicopter control system and the red team attack against it.  I believe there was a proceedings, but all I can find is the program, https://crypto.stanford.edu/jcm60/program.php.  Maybe you'll have better luck.

--------------
Alan Karp

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMxURy0sB5y0Cgi5a9WLG3G257DSyMGTf7u5rgNPtCNFg%40mail.gmail.com.

[Matt Rice]

I would hazard a guess that this is the talk Using Formal Methods to
Eliminate Exploitable Bugs given by Kathleen Fisher Friday, May 20,
2016 3:30pm
as part of the HACMS project https://ts.data61.csiro.au/projects/TS/SMACCM/

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z1zVb3Ywp5TTOPQDp3u146BhbdOJeKeK6YOoyzY%2BYJeaA%40mail.gmail.com.

[Christopher Lemmer Webber]

This, maybe? https://www.researchgate.net/publication/328128004_Formal_Verification_of_Helicopter_Automatic_Landing_Control_Algorithm_in_Theorem_Prover_Coq

Alan Karp writes:

> I was talking about applying formal methods to things like OpenSSL. The
> leverage you'd gain is probably worth the cost if only someone would pay
> for it.
>
> A few years back, I attended a celebration of John Mitchell's 60th
> birthday. One of the talks described the formal verification of a
> helicopter control system and the red team attack against it. I believe
> there was a proceedings, but all I can find is the program,
> https://crypto.stanford.edu/jcm60/program.php. Maybe you'll have better
> luck.
>
> --------------
> Alan Karp
>
>
> On Wed, Feb 10, 2021 at 2:00 PM Jonathan S. Shapiro <
> jonathan....@gmail.com> wrote:
>
>> On Wed, Feb 10, 2021 at 1:37 PM Alan Karp <alan...@gmail.com> wrote:
>>
>>> Jonathan S. Shapiro <jonathan....@gmail.com> wrote:
>>>
>>>>
>>>> I think you're in the wrong order of magnitude by several orders,
>>>>
>>>
>>> I agree for products in general, but what about key libraries,
>>> particularly widely used open source projects? I can imagine the effort
>>> would pay off for everyone. Of course, there's still the question of who
>>> would pay for it.
>>>
>>

>> Since general purpose systems largely defy *informal* specification

>> (never mind formal specification), I think the scope of the current
>> discussion is probably limited to tightly scoped fixed-function systems,
>> inductive algebraic systems, and some types of protocols.
>>
>> My understanding of the state of the art is now a decade stale, but at
>> that time the sweet spot for systems verification was systems with fixed
>> external specifications (feature creep and verification don't mix) and
>> fixed finite resource bounds per instance (though those can be
>> parameterized). If those two constraints both hold, you're essentially
>> dealing with a (potentially very large) state machine. Assuming the
>> property of interest actually holds, you're well within the bounds of

>> feasible mechanized verification *provided* you have adequate compute

>> resources and a suitably talented verification team.
>>

>> The people who build this class of system are largely *systems* people.

>> The overlap between this group and people who understand higher-order logic
>> and/or dependent type systems (which lie at the heart of modern provers)
>> is... small. There's my former group, Gernot's group, some of Hermann's
>> group, some graduates of Frank Pfenning's group, and the group that
>> (literally) saved Mercedes from bankruptcy. There's a group at the Advanced
>> Physics Laboratory that does heavily classified things, and there are
>> comparable teams in Europe. I'm sure there are other commercial teams I
>> don't know about or have forgotten about. But if you're looking at the

>> *intersection* of these skill sets, I doubt very much that the total

>> world supply of candidates reaches 150 souls. Given which, the fact that
>> they aren't high-value hires really tells you something about how their

>> work is *perceived*. At one point there was a fairly good group at NSA,

>> but it appears that they lost the internal resource battle to the crypto
>> nitwits who brought us such successes as Clipper and its friends.
>>
>> No offense to Carl intended or implied by excluding him; I simply don't
>> happen to know how his group's efforts are focused, and I'd appreciate
>> learning.
>>
>>
>>
>> Jonathan
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "cap-talk" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to cap-talk+u...@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMxURy0sB5y0Cgi5a9WLG3G257DSyMGTf7u5rgNPtCNFg%40mail.gmail.com

>> <https://groups.google.com/d/msgid/cap-talk/CAAP%3D3QMxURy0sB5y0Cgi5a9WLG3G257DSyMGTf7u5rgNPtCNFg%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>

[Alan Karp]

Matt Rice <rat...@gmail.com> wrote:

I would hazard a guess that this is the talk Using Formal Methods to
Eliminate Exploitable Bugs given by Kathleen Fisher Friday, May 20,
2016 3:30pm
as part of the HACMS project https://ts.data61.csiro.au/projects/TS/SMACCM/

I believe that's the one.

--------------
Alan Karp

[Carl Hewitt]

The mathematical theory of categories [McLarty 1991] is inadequate for 

the foundations of Computer Science because 

it lacks precision since it is a 1st-order theory.

Every 1st-order theory has nonstandard models, 

which means that the theory has

not precisely defined subject matter of the theory.

On the other hand, the theory Actors has 

just one model up to a unique isomorphism.

See the following for more details:

Pysical Indeterminacy in Digital Computation

        https://papers.ssrn.com/abstract=3459566

Regards,

Carl

https://professorhewitt.blogspot.com/

Regards,

Carl

https://professorhewitt.blogspot.com/

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc2qTYcFYPRC2Tutm7%2BAqK-W%3Dz6oW%2B3-POfBPUyhYYQ68A%40mail.gmail.com.

--

  Cheers,
  --MarkM

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjEYXDOscf9b%3D2YVMR0GnVMaFscknUA76-ubGzZO_K8EQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/0358607b-ef70-4e56-a9b6-662db364c3e2n%40googlegroups.com.

[mostawe...@gmail.com]

Yes, ETCS and ETCC, the *elementary* theories of Set and Cat respectively, are first-order. However, as Bauer explains in "Five Stages of Accepting Constructive Mathematics" (https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf), or Williams and Stay in "Native Type Theory" (https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html), the native language of a topos is a higher-order theory.

This is part of the problem with the word "foundations". Once we have found enough topoi, then we must question exactly how useful our metatheory can be. We can take each desired feature of our metatheory (Boolean, Choice, Infinity, equality, impredicativity, custom axioms) and go find a topos *inside* our metatheory which can re-prove all of the metatheory's statements. But it would just be one topos in a constellation of infinite custom worlds of mathematics. We live in a multiverse of objects, with many different entrances of study. Baez (and Shulman, but Baez in particular has said this many times) emphasizes entrances, not foundations, in their "Lectures on n-Categories and Cohomology" (https://arxiv.org/abs/math/0608420).

Coming back up for air, let's reword the initial claim. Given a metatheory which can do category theory, let Set be the (unique up to unique isomorphism!) free topos with Choice, a natural numbers object, and the well-pointedness property: given any f, g : A -> B, either f = g (in the topos!) or exists p : 1 -> A (the "well point") which distinguishes them. There's no non-standard modelling here. The arbitrariness of the topos, and thus the fact that there's multiple models based on how we arrived at it, is wholly in the metatheory. (This includes the choice of inaccessible large cardinal in the Tarski-Grothendieck axiom.)

A similar story plays out for ETCC. Given a metatheory which can do *higher* category theory, Cat is a 2-topos (https://ncatlab.org/nlab/show/2-topos for details) constructed analogously to Set. Again, there are metatheoretic choices, and those are what give rise to the variety of models. But the topos Cat itself has the same internal language regardless of construction; it gives higher-order logic on categories and functors.

And, finally, for practical day-to-day computer science, we can fix our topos as Eff, the effective topos (construction details at https://ncatlab.org/nlab/show/effective+topos), which precisely turns higher-order intuitionistic logic into computer programs. Indeed, Eff is constructed on Set, and there's an analogous construction for any topos. This is not only theoretical; the MarshallB programming language (paper and notes: https://lobste.rs/s/si5k5i) was built by considering a topos whose objects were interesting primitives for constructive solid geometry, and then using turn-the-crank techniques to flesh it out and implement it in software.

[Carl Hewitt]

Thanks for your thoughts, Corbin.

It may be that a mathematical theory for categories should be higher-order.

However, such a higher order mathematical theory 

has not been published :-(

Even if such a higher-order mathematical theory should be published, 

how would it be possible to prove that there is 

just one model up to a unique isomorphism?

Because of the Actor Event Induction axiom,

the mathematical theory of Actors has 

just one model up to a unique isomorphism. 

Current mathematical theory of categories lack an induction axiom.

Regards,

Carl

https://professorhewitt.blogspot.com/

On Sat, Feb 20, 2021 at 6:51 AM mostawe...@gmail.com <mostawe...@gmail.com> wrote:

the native language of a topos is a higher-order theory.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/94cd8b33-ee88-4bf6-b2f0-6d6336822273n%40googlegroups.com.

[Carl Hewitt]

Strong types are rigorously defined because

there is just one model of the theory of strong types 

up to a unique isomorphism.

Also, strong types are more powerful than categories because 

they can be recursively defined.

Cheers,

Carl

https://professorhewitt.blogspot.com/

---------- Forwarded message ---------
From: Carl Hewitt <carl.e...@gmail.com>

Date: Sat, Feb 20, 2021 at 11:52 AM
Subject: Re: Mathematical theory of categories is inadequate for the foundations of Computer Science
To: cap-talk <cap-...@googlegroups.com>

Thanks for your thoughts, Corbin.

It may be that a mathematical theory for categories should be higher-order.

However, such a higher order mathematical theory 

has not been published :-(

Even if such a higher-order mathematical theory should be published, 

how would it be possible to prove that there is 

just one model up to a unique isomorphism?

Because of the Actor Event Induction axiom,

the mathematical theory of Actors has 

just one model up to a unique isomorphism. 

Current mathematical theories of categories lack an induction axiom.

Regards,

Carl

https://professorhewitt.blogspot.com/

On Sat, Feb 20, 2021 at 6:51 AM mostawe...@gmail.com <mostawe...@gmail.com> wrote:

the native language of a topos is a higher-order theory.

On Tuesday, February 16, 2021 at 6:55:31 AM UTC-8 carl.e...@gmail.com wrote:

The mathematical theory of categories [McLarty 1991] is inadequate for 

the foundations of Computer Science because 

it lacks precision since it is a 1st-order theory.

Every 1st-order theory has nonstandard models, 

which means that the theory has

not precisely defined subject matter of the theory.

On the other hand, the theory Actors has 

just one model up to a unique isomorphism.

See the following for more details:

Pysical Indeterminacy in Digital Computation

        https://papers.ssrn.com/abstract=3459566

Regards,

Carl

https://professorhewitt.blogspot.com/

On Sun, Jan 31, 2021 at 11:14 PM mostawe...@gmail.com <mostawe...@gmail.com> wrote:

"Everything is an actor" implies that there is a category of actors. We can sketch such a category briefly.