Note that dependently-typed code also effectively "runs at compile-time", it's inherent to that programming model. You can "extract" an ordinary program from d

Note that dependently-typed code also effectively "runs at compile-time", it's inherent to that programming model. You can "extract" an ordinary program from dependently-typed code which you can then compile to a binary and run as usual, but then that program will not feature dependent types in their full generality.