I've just came to a twofold realization, which in theory seems to support my longing for a "gradually provable" programming system. Specifically, I realized for some parts/modules of my code, I'd like to be able to slap a proof of a set of known properties on them, and by this, "seal them as done", and by this, just get them off my head, "forever". And in this act, elevate them to a special shelf/closet of "safe tools", stamped as reliable, safe, well understood, shrink-wrapped solutions for particular need.
And notably, I also realized, that it also surprisingly fits into a programming philosophy I've come to see as useful recently. Namely, where programming is seen somewhat similar to a scientific experiment. In that the "sofware design assumptions" form a "hypothesis", and the act of implementation is akin to an "experiment" (~ as understood by the scientific method) -- in that it (the implementation/experiment) attempts to validate or invalidate the hypothesis. Here, I'd see the formal proof as the ultimate phase of the evolution of the idea.
In other words, the parallels that seem sensible to me, if carried over to a gradual typing & proving system:
- dynamic typesystem, for initial prototyping ≈ a "preliminary, qualitative" experiment, to check if the direction is even worth exploring further;
- static typesystem ≈ a later stage, full fledged "quantitative" experiment; takes more work; by act of preparation/implementation of it, one explores the idea deeper and gains better understanding of the problem at hand;
- formal verification/proof ≈ the ultimate stage, where a final theory is developed and tested, and the idea/hypothesis/problem can be seen as fully understood, fully explored, sealed, proven.