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


Skip to first unread message

Carl Hewitt's profile photo
unread,
Jan 24, 2021, 11:11:00 AM (8 days ago) Jan 24
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-...@googlegroups.com
Christopher Lemmer Webber's profile photo
unread,
Jan 24, 2021, 4:38:24 PM (8 days ago) Jan 24
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-...@googlegroups.com, Carl Hewitt
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's profile photo
unread,
Jan 24, 2021, 5:53:59 PM (7 days ago) Jan 24
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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.

Carl Hewitt's profile photo
unread,
Jan 24, 2021, 9:50:17 PM (7 days ago) Jan 24
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to Christopher Lemmer Webber, cap-...@googlegroups.com
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.


Carl Hewitt's profile photo
unread,
Jan 24, 2021, 10:07:37 PM (7 days ago) Jan 24
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to Mark S. Miller, cap-talk
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.

Jonathan S. Shapiro's profile photo
unread,
Jan 26, 2021, 4:03:45 PM (6 days ago) Jan 26
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-talk, Mark S. Miller
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.

Mark S. Miller's profile photo
unread,
Jan 26, 2021, 7:12:07 PM (5 days ago) Jan 26
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-...@googlegroups.com, Mark S. Miller
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.
Carl Hewitt's profile photo
unread,
Jan 27, 2021, 9:42:40 AM (5 days ago) Jan 27
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-talk, Mark S. Miller
Bill Frantz's profile photo
unread,
Jan 27, 2021, 8:41:43 PM (4 days ago) Jan 27
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to cap-...@googlegroups.com
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's profile photo
unread,
Jan 29, 2021, 12:38:16 PM (3 days ago) Jan 29
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
On Tue, Jan 26, 2021 at 4:12 PM Mark S. Miller <ma...@agoric.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.
Matt Rice's profile photo
unread,
Jan 29, 2021, 2:50:37 PM (3 days ago) Jan 29
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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's profile photo
unread,
Jan 29, 2021, 3:46:33 PM (3 days ago) Jan 29
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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:
  • 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.
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.
Carl Hewitt's profile photo
unread,
Jan 30, 2021, 6:16:04 PM (yesterday) Jan 30
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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:SentenceviwEventvSw]                         // 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 SentenceviwEventvSw.
Carl Hewitt's profile photo
unread,
Jan 30, 2021, 6:39:21 PM (yesterday) Jan 30
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
[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:PropositionviwAddresses ]                                                                                  // 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, e1:Scoped Svew] P[AddressInfo[e]]P[AddressInfo[e1]])

                                                                                        // 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.  [e1:Event, e2:Event ] e1e2 AddressInfo[e1]AddressInfo[e2]

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's profile photo
unread,
Jan 30, 2021, 6:48:56 PM (yesterday) Jan 30
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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 ;-)
Mark S. Miller's profile photo
unread,
Jan 31, 2021, 1:02:09 AM (yesterday) Jan 31
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
Carl Hewitt's profile photo
unread,
Jan 31, 2021, 6:56:36 AM (yesterday) Jan 31
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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's profile photo
unread,
Jan 31, 2021, 7:05:31 AM (yesterday) Jan 31
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
mostawe...@gmail.com's profile photo
unread,
2:14 AM (2 hours ago) 2:14 AM
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
"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.