I love this topic. You did a great job breaking this down in a way relatable to programmers. I want to supplement this with one mathematical perspective of this I find interesting.
A way to unify these ideas together is the notion of universal quantification. The model needs to account for all possible values of the "world", so the model is universally quantified over the "world". This can be thought of as a pure function with a "world" parameter and a body implementing the "machine". This is related to how the type (∃ α: P(α)) → β is isomorphic to the type ∀ α: (P(α) → β).
This "world" is the extraction of all the non-deterministic things you mention here. It can be mathematically modeled as a data structure that's input into the system. Here are examples of how each item could be concretely represented in this data structure:
Random numbers can be represented by their seed. The seed can be any possible seed value, and once you have the seed value, the system is deterministic based on that.
User input and external forces can be represented as a stream of events, such as { "event": "click", "x": 1192, "y": 576 }.
Concurrency can be modelled as a stream of "events" specifying the thread to execute the next instruction of. For example, a sequence of events [1,1,2,3,2] would run two instructions from thread 1, then one from thread 2, then one from thread 3, then continue one instruction on thread 2. This is like modeling the OS scheduler as an external force as described in the previous bullet point.
Of course, modelling concurrency like this is very impractical for modeling real systems. This perspective is instead useful for things like the theory of programming languages.
<hr />
Finally, let's address abstraction. Abstraction can be thought of like moving something from the "machine" to the "world", pretending like something in your control is instead out of your control. This universally quantifies over extra things that do not need to be universally quantified.
For your example, you add a function of type Message -> enum{A, B, C} to your "world" input, then use it to replace the complicated implementation from the real "machine". This resembles using dependency injection to replace references to a concrete class with a constructor parameter. This reiterates how function parameters are used for universal quantification.
So yeah, non-determinism, abstraction, and "world vs machine" are all perspectives on universal quantification, which can be mathematically modelled by functional abstraction.
I love this topic. You did a great job breaking this down in a way relatable to programmers. I want to supplement this with one mathematical perspective of this I find interesting.
A way to unify these ideas together is the notion of universal quantification. The model needs to account for all possible values of the "world", so the model is universally quantified over the "world". This can be thought of as a pure function with a "world" parameter and a body implementing the "machine". This is related to how the type (∃ α: P(α)) → β is isomorphic to the type ∀ α: (P(α) → β).
This "world" is the extraction of all the non-deterministic things you mention here. It can be mathematically modeled as a data structure that's input into the system. Here are examples of how each item could be concretely represented in this data structure:
Random numbers can be represented by their seed. The seed can be any possible seed value, and once you have the seed value, the system is deterministic based on that.
User input and external forces can be represented as a stream of events, such as
{ "event": "click", "x": 1192, "y": 576 }.Concurrency can be modelled as a stream of "events" specifying the thread to execute the next instruction of. For example, a sequence of events
[1,1,2,3,2]would run two instructions from thread 1, then one from thread 2, then one from thread 3, then continue one instruction on thread 2. This is like modeling the OS scheduler as an external force as described in the previous bullet point.Of course, modelling concurrency like this is very impractical for modeling real systems. This perspective is instead useful for things like the theory of programming languages.
<hr />Finally, let's address abstraction. Abstraction can be thought of like moving something from the "machine" to the "world", pretending like something in your control is instead out of your control. This universally quantifies over extra things that do not need to be universally quantified.
For your example, you add a function of type
Message -> enum{A, B, C}to your "world" input, then use it to replace the complicated implementation from the real "machine". This resembles using dependency injection to replace references to a concrete class with a constructor parameter. This reiterates how function parameters are used for universal quantification.So yeah, non-determinism, abstraction, and "world vs machine" are all perspectives on universal quantification, which can be mathematically modelled by functional abstraction.