This is one of the things I love about CoqIde compared to other REPL-environment IDEs. You basically play your input file like a movie: scrubbing back and forth

This is one of the things I love about CoqIde compared to other REPL-environment IDEs. You basically play your input file like a movie: scrubbing back and forth, rewinding to edit the past, skip to the end, etc. Half the screen is dedicated to a debugger-like display exposing information about the state of the program at that moment in time. This has an entirely different mechanism of action but I can see it enabling the same excellent workflow and usability for imperative code with a filesystem, etc. and that's awesome.