ProfHewitt

ActorsTheory serves as the rigorous mathematical foundations of capability systems.

Foundation is about rigorously specifying the general Laws of Locality for Actor systems that CHERI implements.

Great to see further progress on CHERI!

See the following for theoretical foundations for the work:

Linux 60th Anniversary Keynote

https://t.co/IRe3vpMlWn

Interesting article.

Mathematical foundations are needed that are much more suitable to modern Computer Science than using "universes".

For an example see the following article:

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

Also, see the following video:

https://www.youtube.com/watch?v=AJP1VL7shiI

Computer science theory didn't get harder.

Instead, education became weaker :-(

See following link for foundations of computer Science:

https://www.youtube.com/watch?v=AJP1VL7shiI

The Actors Abstraction does not require specification of

computer boundaries.

The Actors Abstraction is foundational for computer science

analogous to the Natural Numbers in classical mathematics.

Probably not a good idea to burden application programmers

with having to annotate each message send with whether the

receiver is on the current computer or another one in a

Citadel.

Since Actors can move between computers in a Citadel, such

annotations are infeasible in practice.

Of course, modularity, security, and performance should not be

ignored.

See the following for a rigorous definition of the Actors Abstraction:

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

Probably can't make much progress without a scientific foundation including the Actors Abstraction.

The Actor Paradigm is much more widespread with offerings from Microsoft, Lightbend, etc.

I fondly remember Joe Armstrong, who was a good friend.

However, not having a mathematical foundation has been a

severe limitation for Erlang.

The Erlang community is trying to dig its way out with

modifications and extensions. Still have a long way to go.

Of course, no Actors framework is perfect.

Many important implementations have been done Erlang.

Also, significant Erlang projects are ongoing to good effect.

Erlang has absolutely no security :-(

In a Citadel, distributed Actors are going to be necessary.

See the following:

    Citadels: faster response time and better information integration than remote datacenters 

Also see offerings from Lightbend and Microsoft.

Erlang incorporated some of the ideas of the Actor Abstraction

but missed a few things. See

See article and video here:

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

https://www.youtube.com/watch?v=AJP1VL7shiI

Swift Actors are an important contribution to the Actor Paradigm.

There is is an upcoming keynote address on the Actor Paradigm at the Linux 30th Anniversary Conference. See

https://reactivesummit2021.sched.com

Both ASIO and Sender/Receiver are not a suitable foundation for concurrency in C++.

As dueling co-routine proposals neither ASIO nor Sender/Receiver are a suitable foundation for C++ semantics.

Async co-routines are not a suitable foundation for C++ semantics.

The Actors Abstraction is a much simpler and more powerful for

formalizing the semantics of C++. See the following:

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

https://www.youtube.com/watch?v=AJP1VL7shiI

Slowing of progress in Science and Technology results from

1. Slowing of scientific processes

    Article is correct that high-quality science is still       
    being performed. Because of increasing noise caused by 
    enormous size, ground-breaking work is increasingly 
    ignored

    In fields like Computer Science, a huge gap has opened 
    between fundamental work and the short-term development 
    horizons of companies.

    Fundamental development can require Apollo-scale projects.
    For example, 
       * resilience against cyberattacks based on the Actors 
         Abstraction and proving systems properties by
         Event Induction
       * Intelligent Systems using electronic glasses and
         Active Ontologies

Contrary to the article discussed in these postings, having

true but unprovable propositions in foundational theories of

mathematics does not place any practical limitations on

scientific knowledge.

The Continuum Hypothesis is still an open question in

foundational mathematical theories that are more powerful

than 1st-order ZFC such as the theory Ordinals.

See the following:

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

Someday, the Continuum Hypothesis might be proved or it

might be disproved in foundational theories.

In foundational theories of mathematics, the following

kind of proposition is true but unprovable:

     Theorems are enumerable by an algorithm.

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

https://www.youtube.com/watch?v=AJP1VL7shiI

In foundational theories, the proposition

I'mUnprovable (used in the proof in [Gödel 1931]) does not

exist because of restrictions on orders of propositions that

were introduced by Bertrand Russell to prevent logical

contradictions in mathematics.

The halting problem provides examples of true but unprovable

propositions because there are some expressions that do not

halt but it is unprovable that they do not halt.

Theorems of a foundational system are not computationally

enumerable (in fact they are not even countable). See the following article:

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

In a foundational system, there are true propositions that

cannot be proved. For example, is true but unprovable that

an algorithm can enumerate the theorems of an order

abstracted from strings.

It turns out that foundational mathematical systems can prove their own consistency.

See the following:

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

However, the proof is not convincing because the proof is

valid even if the system is inconsistent!

[Gödel 1931] proposed the proposition I’mUnprovable (such

that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential

undecidability of Russel’s foundational theory, which had the

type-restriction on orders of propositions to prevent

inconsistencies. I’mUnprovable cannot be constructed in

foundational theories because strong types prevent

construction of I’mUnprovable using the following recursive

definition (see Diagonal Lemma [Gödel 1931]):

I’mUnprovable:Proposition<i>≡⊬I’mUnprovable.

Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because

I’mUnprovable:Proposition<i> is a propositional variable in

the definition ⊬I’mUnprovable. Consequently,

I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1>,

which is a contradiction.

Bertrand Russell introduced orders on propositions to block

construction of paradoxes such as “The Liar” [Russell 1908].

Without orders on propositions, the “self-referential”

proposition I’mFalse (such that

I’mFalse⇔¬I’mFalse) could be constructed using the

following recursive definition:

I’mFalse:Proposition<i>≡¬I’mFalse. Since Ψ is a

propositional variable in the definition, ¬Ψ:Proposition <i+1>. Consequently,

I’mFalse:Proposition <i>⇒I’mFalse:Proposition<i+1>, which

is a contradiction.

For more information see the following:

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

https://www.youtube.com/watch?v=AJP1VL7shiI