It might be helpful to look at something like Typescript Tic Tac Toe in the type system [1]. You can comment out individual lines in the GameLoop type, and then hover over `____________DISPLAY___________` to see the current game state. Illegal moves will result in type errors.
Running Doom in the type system effectively means a lot more types have been generated (effectively a C to typescript-type compiler was created if I understood this correctly), then the game was started with no inputs entered. Theoretically if the author had infinite time and compute resources, the history of control inputs up to a certain point in play could be put in a tuple, and the type system would generate the state of the game given the code and the moves which the user had input so far. This state would include what's on the screen, but also internal state variables controlling things like where the enemies were moving, whether projectiles are in air, their direction, collision detection, etc.
Running Doom in the type system effectively means a lot more types have been generated (effectively a C to typescript-type compiler was created if I understood this correctly), then the game was started with no inputs entered. Theoretically if the author had infinite time and compute resources, the history of control inputs up to a certain point in play could be put in a tuple, and the type system would generate the state of the game given the code and the moves which the user had input so far. This state would include what's on the screen, but also internal state variables controlling things like where the enemies were moving, whether projectiles are in air, their direction, collision detection, etc.
[1]: https://tsplay.dev/wE95vw