Virtual Meetup - Building a Typed, Concurrent Programming Language with Racket

Hi Community,

I am happy to announce that this Thursday (the 19th of May), Sam Caldwell will hold the discussion about " Building a Typed, Concurrent Programming Language with Racket​ ".

Also, remember that we changed the link to join the Meetup!

Concurrency is a necessity for many applications but unfortunately makes designing and understanding programs difficult. In response, numerous linguistic models have arisen that define what a concurrent program is and how such components interact. In this talk, I will present the dataspace model of actors, which seeks to improve the ability to share information among groups of isolated, actor-style entities.

Concurrency models, such as dataspace actors, primarily address the run-time organization of programs. This run-time organization arises from a static description, i.e. the composition of some forms provided by a language or library. For this purpose, the dataspace model includes a domain-specific language (DSL) for programming actors. This language of facets allows directly articulating the primary programming concerns of dataspace actors: maintaining local state, sharing information with other actors, and engaging/disengaging in behaviours.

Developing communicating programs, such as dataspace actors, requires designing and implementing protocols. Type systems are a natural tool for assisting programmers in this task. To this end, a typed dialect of the facet language can help programmers check their programs against their protocols. By using techniques from behavioural type systems, communication properties for actors written using this typed language may be specified in temporal logic and then verified using a model checker.

Sam Caldwell is a PhD student at Northeastern University in Boston. Before. starting his PhD, he was a computer engineer and worked for a smart light
startup. He is interested in designing programming languages and tools for building comprehensible concurrent systems.​​

How to connect

To avoid other security issues is now necessary to register for the meeting. The registration should be necessary just once and be valid for all the next meetings you will participate in. I understand it is a little extra effort, but it would avoid problems like the ones we encountered:

Registration for the Virtual Meetup

After registering, you will receive a confirmation email containing information about joining the meeting. It will also permit you to add it to your calendar.

Time

It is hosted on Zoom at 6 PM GMT+1/CEST (you can use this link to figure out which time is in your timezone: Dateful Time Zone Converter).

Cheers,
Elisa

P.S. We get a recurring question: “Are presentations recorded?”. The answer is not, and the reasons are explained here On recording Virtual Meetups - #7 by voelter

Some links about this meetup by Sam Caldwell:

Here there is the content of the chat:

18:00:05 From Mike Cargal to Everyone:
	quick... make up a story…
18:06:42 From Jürgen Mutschall to Everyone:
	How do you compare your approach to tuple spaces and LINDA?
18:10:02 From Steffen Zschaler to Everyone:
	I had a similar question. This slide seems to suggest that the dataspace is more like a shared state space than the typical tuple space being used for work items. How does this relate to blackboard pattern?
18:12:14 From Peter Wasilko to Everyone:
	Does the pattern matching use Unification?
18:15:04 From Peter Wasilko to Everyone:
	That would be most appreciated!
18:18:08 From Steffen Zschaler to Everyone:
	How does the light know which switch to subscribe to?
18:18:57 From Mariusz Postół to Everyone:
	Is publisher/subscriber 1:1 relationship?
18:19:09 From Steffen Zschaler to Everyone:
	So is there a notion of dynamically creating queries or do they need to be statically defined from the start?
18:19:44 From Peter Wasilko to Everyone:
	Could the light request that an IO Device query the user?
18:20:21 From Peter Wasilko to Everyone:
	(e.g. Have Siri ask what room the new light is in.)
18:21:55 From Steffen Zschaler to Everyone:
	Apologies!
18:22:17 From Federico Tomassetti to Everyone:
	no reason to apologize, the discussion is very interesting!
18:24:10 From Mariusz Postół to Everyone:
	Talking about communication are we talking about runtime or alternatively about design time?
18:24:41 From Peter Wasilko to Everyone:
	Wouldn't the switch have to make the light removal notification if flipping it killed the light's com functionality?
18:25:26 From Peter Wasilko to Everyone:
	Is something polling the light to make sure it is still alive?
18:28:33 From Steffen Zschaler to Everyone:
	How does the light know what "labels" are available to subscribe to? (Do the light manufacturers need to agree with the presence-sensor manufacturers that room-empty is a meaningful label?)
18:28:59 From Rene to Everyone:
	No endpoints or Topics to deal with, I like this
18:29:07 From Peter Wasilko to Everyone:
	If the light fails maybe the system could turn on a TV and set it to digital photo frame mode with a white background.
18:29:21 From Steffen Zschaler to Everyone:
	Rene, the topics are the labels, aren't they?
18:30:33 From Rene to Everyone:
	I guess so, but I wouldn't have to manage and create and deal with topics. the labels here look like message types to me.
18:30:54 From Gregg Irwin to Everyone:
	I think the details are necessarily simplified for the presentation, and short time available.
18:32:57 From Peter Wasilko to Everyone:
	Are the comments machine readable documentation?
18:35:16 From Steffen Zschaler to Everyone:
	So, really actors get all events and then filter out the ones they're interested in?
18:36:49 From Gregg Irwin to Everyone:
	I'll hazard a guess that the router filters, and what we see here is just the actor switching. They could also subscribe to * and have an 'else handler.
18:36:51 From Mariusz Postół to Everyone:
	Usually talking about pub-sub we are talking about subscribing to a topic. Is assertion a kind of topic?
18:37:03 From Peter Wasilko to Everyone:
	Do the lights have the ability to run racket programs, so they could blink in high speed morse code to transmit data?
18:38:13 From Gregg Irwin to Everyone:
	Lights here are make-believe, so could do anything. This is just about how they communicate through the dataspace. Sam can correct any mis-guesses I make. :^)
18:39:57 From Steffen Zschaler to Everyone:
	@Gregg: All I saw was pattern matching logic inside the actor, not a set of declaratively specified patterns to subscribe to, so wasn't sure how the dataspace would be able to pre-filter.
18:40:32 From Steffen Zschaler to Everyone:
	But possibly, this is something that the DSL does by making on tell the dataspace?
18:41:05 From Gregg Irwin to Everyone:
	Yeah, he may get to that detail.
18:41:43 From Gregg Irwin to Everyone:
	There's the subscription answer. :^)
18:41:48 From Steffen Zschaler to Everyone:
	Indeed
18:43:59 From Steffen Zschaler to Everyone:
	Very nice
18:44:14 From Steffen Zschaler to Everyone:
	Can you say some more about what happens under the hood?
18:44:14 From Rene to Everyone:
	I'm confused, but that's ok! =)
18:45:56 From Jürgen Mutschall to Everyone:
	What is your research goal defining this language?
18:47:49 From Gregg Irwin to Everyone:
	It looks like each actor comes to life and automatically gets a mailbox in the dataspace (its channel), and there are predefined elements (field, assert, react, etc.) over what a generic tuplespace would offer, i.e. the routing.
18:50:44 From Rene to Everyone:
	Are the endpoints created at runtime, or compile time? Ok, compile time it looks like.
18:51:21 From Gregg Irwin to Everyone:
	Could be either, because endpoints come and go in the space, right?
18:51:31 From Mariusz Postół to Everyone:
	My point is that syntax is a set of rules we are using to assign meaning to the text valid against syntax. Is it possible to harmonize our definitions?
18:53:22 From Gregg Irwin to Everyone:
	OK, maybe it's that macro expansion is compile-time, but endpoints are runtime constructs.
18:53:59 From Mariusz Postół to Everyone:
	Sorry, the question should be: My point is that semantics is a set of rules we are using to assign meaning to the text valid against syntax. Is it possible to harmonize our definitions?
18:56:47 From Rene to Everyone:
	Your are a master good sir!
18:56:53 From Steffen Zschaler to Everyone:
	The question above about research goal was interesting.
18:57:17 From Steffen Zschaler to Everyone:
	It's an internal DSL, Paul.
18:58:21 From Steffen Zschaler to Everyone:
	What are the benefits of doing this as an internal DSL in Racket rather than as a separate standalone language?
18:59:52 From Peter Wasilko to Everyone:
	So you could create a reader for an arbitrary surface structure as long as it returns a symbolic expression for use by the other tooling?
19:02:44 From Peter Wasilko to Everyone:
	Is there a paper we can read on facets?
19:03:23 From Steffen Zschaler to Everyone:
	Can you subscribe to complex events?
19:06:00 From Gregg Irwin to Everyone:
	Macrology. Fun word. :^)
19:07:00 From Peter Wasilko to Everyone:
	can you back up over the last couple of slides you skipped over?
19:07:32 From Rene to Everyone:
	I'll have to do some Racket coding some time
19:07:56 From Tomas Öberg to Everyone:
	Thank you for a great presentation!
19:08:04 From Gregg Irwin to Everyone:
	Thank you Sam!
19:08:08 From Jürgen Mutschall to Everyone:
	Thank you very much!
19:08:17 From Peter Wasilko to Everyone:
	Thank you so much!
19:08:23 From Patrick Park to Everyone:
	Thanks, very interesting!
19:08:27 From Rene to Everyone:
	Good presentation
19:09:12 From Mariusz Postół to Everyone:
	Great job, thanks.
19:09:51 From Meinte Boersma to Everyone:
	Nice presentation! Have to leave already, unfortunately.
19:09:59 From Federico Tomassetti to Everyone:
	Thank you Meinte!
19:10:02 From Herman Peeren to Everyone:
	Is there any handling for concurrent conflicting assertions? For instance switch on and off at the same time?
19:10:51 From Sam Caldwell to Everyone:
	https://syndicate-lang.org/tonyg-dissertation/
19:11:18 From Peter Wasilko to Everyone:
	Or lights in a room with a presence sensor
19:12:39 From Mariusz Postół to Everyone:
	Conflicts mean that there is a critical section. Is there any support on how to avoid deadlock, and data integrity?
19:13:21 From Mike Cargal to Everyone:
	that's a bit of the crux of what makes concurrent programming hard though, isn't it?
19:13:36 From Gregg Irwin to Everyone:
	If it's like a tuplespace, that's fundamental to the system design, but here only an actor can write to it's on channel.
19:14:28 From Steffen Zschaler to Everyone:
	But channels aren't very meaningful, right, because everything then gets broadcasted to everyone else without any channel ID.
19:14:46 From Gregg Irwin to Everyone:
	So it's a single writer, and the routing likely dispatches events serially, or they go into the mailbox and the actor processes them serially.
19:15:25 From Steffen Zschaler to Everyone:
	But that might still mean that if different actors assert conflicting statements that other actors see them in different orders.
19:15:26 From Gregg Irwin to Everyone:
	I *think* the assertions create the idea of channels.
19:15:34 From Paul Spencer to Everyone:
	many thanks and good luck with your PhD!
19:15:42 From Gregg Irwin to Everyone:
	Nice to see you all!
19:15:45 From Glen Braun to Everyone:
	Thank you!
19:15:55 From Tomas Öberg to Everyone:
	Thank you!