Turing machines only model mathematical functions. They cannot model anything on my list. That's why computer scientists invented I/O automata in an attempt to build a theoretical model that handles some of those items on my list.
> “oh, that’s obviously stateful and imperative” merely because they haven’t thought about the problem in a different way.
It doesn't need to because it's implementation details.
Where it's needed such as in modelling the very important implementation detail of parallelism on multi-core machines to ensure correctness (such as with model checkers like Spin) then stuff like buchi automata are used, but that's dragging maths into the real world to solve real world problems. Turing machines don't live in the real world.
We know a Turing machine can't model all aspects of concurrency because a Turing machine with threads can compute an integer of unbounded size while there's always a bound on the greatest integer an unthreaded Turing machine can.
But this is all naval-gazing anyway. What's even the point of a purely-declarative OS when it's either gonna:
1. Act as a glorified C preprocessor for an imperative language like Haskell and its do-notation?
Haskell with do-notation is not imperative, that’s a common misconception. It’s a special syntax for working within a monad that desugars to nested function calls.
Typically declarative systems are interesting because it is easier to prove strong properties about them.
I agree. Declarative systems are interesting. I am not against studying, implementing, or understanding declarative OSes from an intellectual viewpoint. Rather, people generally speaking ignore that the declarative perspective is not teleological and doesn't reflect the teleology of an underlying OS.
Imperative programs are so popular among "joe schmoe" average programmers because they have a clear teleology. People are willing to forgive that imperative programs are harder to formally reason about because they make the teleology clearer. But have you seen declarative code? Because it's like math formulas, each function needs the same kind of documentation in order to understand the teleology behind the function.
> “oh, that’s obviously stateful and imperative” merely because they haven’t thought about the problem in a different way.
No I am not a conventionalist.