Differentiable programming should be dependently typed. That is, I should be able to state the tensor shapes used in various operations and have the compiler catch my errors if I wish.
-
That's precisely what we do with Keras models: any model that compiles, will run. Shape/dtype/connectivity errors are caught statically before running the actual graph (albeit that's still a python runtime)
Compilation is itself a runtime, by definition. In the case of Keras models, the compilation runtime is the Python interpreter, which is a bit strange perhaps, but works well for our purposes...
