Dependent types acting as a specification that does not force the user to provide a proof and is partially checked at runtime, is a necessary requirement for their use.
There are many use cases here, I need to do some studying, for example it enables the execution of unfinished programs, something that the hazel research group has? Implemented.
Some questions I have:
Can the error be pinpointed to the specific function that was wrong?
To have a live programming environment, we need to have a concept of an ephemeral function, meaning that function f1 is erroneous, an exception is triggered, one fixes the error that leads to function F2 and then the execution continues without stopping the program, without invalidating previous results.
In other words a function needs to be a stream of functions, so to speak.
I believe that it will take many years for this to be implemented. The mathematical community does not want this feature. Maybe easier, less general solutions exist.