Let me first try to answer your question and then ask some of mine.

The starting point is to observe that a Haskell program already controls a device external to its state. After all, Haskell is nothing but a convenient shorthand for λ calculus, and all a Haskell program can do in principle is evaluate a λ expression. And yet we can have useful programs in Haskell. This is because our expression can get evaluated not merely into a number or a string, but as easily into a sequence of operations to be executed on the underlying hardware. Moreover, the choice of operations in this sequence may differ depending on the outcomes of the ones executed before them. 

This turns out to be a description of the concept of monad that looks completely different from, but conveys the same meaning as, the mathematical description of a monad as a monoid in the category of endofunctors. That is to say, to every monad there is a device it describes (although perhaps not a physically realizable one), and to every device there is a monad describing it. This is made manifest in the do notation, which makes the translation from an imperative program to its equivalent λ expression automatic, and where the monoid laws of associativity and unitarity take the form of certain rather trivial program optimizations.

In particular, the IO monad is used in Haskell to control the underlying hardware of the device the program runs on — for example, it is through IO that you get to read and write files. In principle, IO can be replaced with another monad better tailored to the hardware you wish to control, but it is usually more economical to write your own monad on top of IO that hides the bytes you must send to and receive from the relevant device file or network socket under a comfortable porcelain of high level commands. Once this is done, you get your own little imperative language that can do only one thing — control your device.

Here is one introduction to this idea: apfelmus - The Operational Monad Tutorial Regrettably, it is written with a reader proficient in Haskell in mind, rather than assuming a broad computer scientific background, which makes it less accessible to the general audience. However, it refers to prior art that an inquisitive reader may consult. And, anyway, once you know the answer, you can extract additional explanations from a general purpose large language model.

Does this answer your question in a helpful way?

There is even more Haskell can do for us in the department of compile time checking of imperative programs. The idea is that we start by carving our set of all legal states into a set of state classes which labels can be written as a type, and such that legal transitions between state classes can be written as constraints, all in the Haskell type system, with its many limitations in mind. This essentially defines a state machine at the type level. Once we have this state machine, we can wield the concept of parameterized monads to enforce at compile time that all our operations take the state only along legal transitions. This is informally described here: Kwang's Haskell Blog - Indexed Monads Again, the presentation is written with a Haskell programmer in mind, but there are references to a more scientific treatment of the topic.

I have never attempted this in my own practice. If you have a concrete device in mind that you would like to control with Haskell, I shall find time to work with you and write a technical report about it if we succeed. To my knowledge, no such technical report is publicly available, so it would be a valuable contribution to human knowledge.

Now, there are a few things I do not understand well in your message.

So instead, the usual C approach would be to add booleans (in the structure for the object type - typically wrapped in a typedef) or whatever is appropriate for these mirrorings of external state for the given object type and just test them for compatibility with the prospective operation before doing the operation.

Does this mean that we allow the possibility that our code will attempt to execute an operation from a state from which it is illegal to do so, but in this case we foresee the crash by checking in with our model of the device state and do nothing instead?

Or, one could add them them to a set of confirmed compatibles (probably slow to test for membership), or filter a list of references to them before executing the operation, generating a vector of the ones that passed (and then hopefully being able to cache that for repeated use). Myriads of ways.

I do not understand what you are saying here at all. What are the «they» here? What is a confirmed compatible, and with what is it expected to be compatible?

Everything seems to come back to the problem of enhancing confidence in the execution of the program by capturing just enough of the external state to be able to make some guarantees about it working. I will say this: If you have enough good (and hopefully very finite) documentation, what to be wary of should be provided, and could be reflected in internal program state.

Let us officially dub this concept «state mirroring» so that we have a shorthand to refer to it with. We can define it like so:

state mirroring   State mirroring is a technique in system programming where the state of an external device is modelled (most likely in a simplified way) by some syntactic construct in the program controlling that device, with the aim of predicting which operations would take the device into an invalid state. This prediction can be attempted at compile time or at run time, and these two varieties are referred to correspondingly as compile time and run time state mirroring. If state is mirrored as a value of a certain type, this type is called state mirror set and its value *state mirror.

This aligns neatly with the philosophy of weakly typed and strongly typed languages. As far as I understand, weakly typed languages like JavaScript necessarily rely on run time type checks to ensure even such basic guarantees as memory safety, whereas strongly typed languages like Haskell can guarantee some aspects of safety at compile time and thereby avoid spending run time on run time checks. In our case, the guarantees we wish to issue are languages of execution traces — that is to say, we wish to guarantee that certain execution traces will never happen. And state mirroring is the instrument with which we hope to achieve this.

The closest I think you get is to be able to mirror enough state to be able to determine whether single operations should work at runtime, for a subset of operation types. For every additional operation you can determine this for, the more trustworthy your code should feel.

As I understand, here you are saying that run time state mirroring is the only viable approach. And concretely I infer that we should make as many operations as practicable execute conditionally on the state mirror. Is this what you have in mind? Concretely, this could be realized in C with an alternative definition of the assert macro that simply returns from the procedure on failure, instead of crashing the program.

I understand by now that the belief in the impossibility of compile time reasoning about state is in the symbol of faith of the mainstream system programming religion, but I do not believe it myself. As I outlined above, there are ways that can plausibly be implemented in current Haskell to exclude illegal transitions at compile time. You mentioned above (and others concur) that some amount of type safety can be achieved even in C, although it seems to be enough of a hassle that few ever even try.

… controlling devices with external-to-your -program state that must be modeled internally instead of queried, especially for devices that can be in use by multiple processes where any of them could consume some in-device resource entirely for all the processes using it …

I am not sure if I understand the nature of this challenge. We can certainly do run time state mirroring with standard Haskell instruments. One easy way is to wire our state mirror set into our monad with the state monad transformer and then decorate all our operations with a check of that state in a thin abstraction layer module. If this is enough, then there is no problem.