I think we might potentially be looking at this backwards. There is a great talk by Jack Rusher [1] on why having really slow iteration loops and being too disconnected from running programs creates a desire for theorem proving because it becomes the faster way to arrive at a correct solution.
I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD.
Not what I'm advocating and certainly not REPL. When I'm talking about a live environment, I mean something _like_ Pharo [1]. I'm arguing against long compile and deploy loops, not formal verification.
I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD.
[1] https://www.youtube.com/watch?v=8Ab3ArE8W3s