Thethirdweb.net Subodh Sharma is a professor of computer science at IIT Delhi, one of the most prestigious universities in India. While he's not teaching, Subodh conducts research into the formal verification of distributed systems, and his work on the automated formal verification of smart contacts has drawn international interest. I called up Subodh because I was looking for someone to explain an approach to writing software called the actor model. The actor model essentially involves sandboxing tasks in such a way that complexity is minimized and all behaviors of a software system can be known under all conditions. Currently the actor model is applied to the management of telecommunications networks through the Erlang language, and also in secure servers. Understanding the way robust distributed systems are constructed assists in the assessment of platform designs and gives us a view into the future of the ultimate distributed system - the Third Web. What is the actor model, what are its origins, where is it usedMessage Passing Interface (MPI) is very similar - is a standard for communication between processors.The Actor Model is an abstract model of computation for capturing concurrent interaction in a system.An actor is a primitive entity of computation.An independent component of a system with its own address spaceLike an object or a taskActors are not like threads which communicate via shared memoryActors communicate via explicit messages.Every actor has an addressCommunication is asynchronousAllowing concurrent execution and message passing Why is concurrent execution and message passing so challenging?Concurrency is difficult to reason about because there is so much to take into account.If the order of arrival of messages from a number of worker processes to a manager process effects the correctness of the manager process output, every possible order of arrival needs to be considered by the programer. DeterminismOutput determinism means that for a given input to a program the output is always the same.Non-determinism allows higher performance. Determinism is easier to reason about.The actor model allows us to have non-deterministic message passing inside a system but maintain deterministic output.Deterministic messaging involves the sender announcing their intention to send a message and the receiver announcing their intention to receive the message from the sender.Non-deterministic messaging is where the receiver does not care where the message is coming fromThis requires all entities to have names or addresses. Where is this used?In telecommunications networks.Also in secure servers.Scientific computing.And because in blockchains all entities have names/addresses, it is an environment that is ideal for actor model based programming. Smart ContractsNothing more than software modulesTransactional in natureEither the transaction meets specifications or it does notSmart contracts must execute deterministically and be oblivious of the environment in which they are running. History of the Actor ModelMid 70sIrene Greif, Gul Agha laid the foundations for the model.Large community of non CS engineers - aerospace, bioscience, chemical engineering - adopted the MPI for scientific programming. MPI was influenced by the actor model.Applications existed for concurrency. The complete system needed to be developed for this to emerge. Subodh's work on autonomously verified smart contractsProvided sound guarantees of bug free codeTook smart contract source code & created a semantic preserving translation to an intermediate language that was verification friendlyThe translated program preserved all of the behaviors that could have emerged in the original.Feed this to an automated tool that performs symbolic model checking.Analyzed smart contracts in generality.Found many buggy smart contracts. Thethirdweb.net