I have been telling people that we need to work on guided synthesis over verification. I believe that guided synthesis is the only way we are going to be able to create correct programs in practice. Verification is just too hard, because you have to write the actual program, write the specification, and then develop the verification proof. Maintenance is difficult, because if any of these parts change you have to update the other two. I think that guided synthesis would work better, because you can write do the specification, then write down the steps and designs to convert it into efficient code. I can imagine doing maintenance on such a structure. It would feel like programming to me, given the right tool support.
In the short term, I think we need to focus on specialized executable specification languages.
The Ultimate Honda
7 years ago
Posts
