> Gradual programming is the programmer tracking the co-evolution of two things: 1) the syntactic representation of the program, as expressed to the computer via a programming language, and 2) a conceptual representation of the program, inside the mind. In the beginning of the process, the programmer starts with no syntax (an empty file) and usually a fuzzy idea of how the final program should work. From this point, she takes small steps in building components of the program until the final version is complete.
Here you first specify your program at a very high level in logic; then you refine the model, still in logic, and proving that the refinement is valid; you iterate some more refinement steps, i.e., you gradually make parts more concrete by actually implementing individual operations; and at the end you have a complete, executable program. A program that, since you proved all the refinement relations as you progressed, is also formally verified against its spec.
Of course this is too much work for most domains, and many domains don't even have any useful notion of formal specs. Also, the actual B system is a horrible thing with a horrible logic and horrible proof tools. But the general idea is appealing, for some things.
> Gradual programming is the programmer tracking the co-evolution of two things: 1) the syntactic representation of the program, as expressed to the computer via a programming language, and 2) a conceptual representation of the program, inside the mind. In the beginning of the process, the programmer starts with no syntax (an empty file) and usually a fuzzy idea of how the final program should work. From this point, she takes small steps in building components of the program until the final version is complete.
calls to mind things like the B-Method (https://en.wikipedia.org/wiki/B-Method).
Here you first specify your program at a very high level in logic; then you refine the model, still in logic, and proving that the refinement is valid; you iterate some more refinement steps, i.e., you gradually make parts more concrete by actually implementing individual operations; and at the end you have a complete, executable program. A program that, since you proved all the refinement relations as you progressed, is also formally verified against its spec.
Of course this is too much work for most domains, and many domains don't even have any useful notion of formal specs. Also, the actual B system is a horrible thing with a horrible logic and horrible proof tools. But the general idea is appealing, for some things.