"Proofs are programs" as in Curry-Howard seems to mostly make sense if you think of programs as having an input and an output like "A to B" which in logic corresponds to having one premise and one goal conclusion
But it might also make sense to think of programs as proof assistants that are open-ended so the user is playing around with rules and resources without aiming for one particular conclusion
Of course you can model this with co-functions and keep the Curry-Howard equivalence, but somehow this seems to be related to a divide in programming culture between interactive dynamic systems and static determinate functions
So an idealized Haskell program is basically one pure value with a specific deterministic proof term, while I want to think more that a program is a collection of resources and rules available for the user to play with at their leisure, also to modify
So a logical formalism or programming language would not just be an implementation technique for "apps" that have nothing to do with logic or programming, but instead we turn the computing environment into a system whose logic is part of the affordances provided to the user
Basically the "proof assistant” as an overarching metaphor for a general purpose computing environment. "Static typing“ will not be just an error-preventing implementation technique, but a framework for reasoning and executing within the computing environment
Like living your life inside Emacs, but instead of Emacs it's a gamified version of a linear logic proof assistant
Existing proof assistant technology might find it relatively easy to handle incremental stepwise reasoning within a concrete common sense world, even though they're measured by success at extremely polymorphic advanced higher order logic
Like you don't need to automatically discover Gödel's ontological proof of God's existence in modal logic, just maybe figure out that you can convert an MP3 to FLAC by first converting to WAV, or that you can solve for both hunger and coffee by going to the local café
