raph, The important question about automated proof checking, is will it improve the practice of Mathematics, and in your case will it improve the practice of programming?
I believe the main things lacking in the practice of programming today are the lack of good problem solving skills, and clear ideas about software's function and purpose. If basic competence of programmers could be cultivated that would be a large step forward. To believe programmers are going adopt a level of rigor even greater than that of professional mathematicians is quite far fetched, at least in near future.
To some extent, I think projects like GNU/Linux help cultivate bad programming practice. There is an effort to create libraries for every concievable problem. Now, I'm not against reuse, I think reuse is good practice, but perhaps reuse should be on level of ideas and algorithms, instead of sets of functions and data structures. Programmers don't evaluate the code they are using. How well does it really solve the problem, how close is the solution to the actual problem they wanted to solve? Developing problem solving skills natually leads to a precise understanding of the function of code.
Language also contributes great deal to the level of rigor of the programmer. The dominant language of GNU, the language which serves as the foundation for all other software of GNU, is also one of the most intelectually lazy languages of the lot. I'm talking of course of the C language, examination of ANSI standard shows the true fuzziness of the C language semantics. How is a programmer expeced to be precise in a language when the language designers wern't precise in it's creation. What percent of C language programmers understand the precise semantics of the language?
Then there is the issue of design, too much design is layed out in advance, too much design is taken for granted. When is a programmer ever given a clean slate? Linux serves to abstract the hardware. Hardware is viewed as something grotesque, to be covered up. To some exent I agree, but Linux is not an overwhelming improvement. File systems are the single most overused overated abstraction in existence and also the most taken for granted. The OS is the creatation of a programmer designed to protect other programmers from their actions. Hardware designers express similar motivations in their hardware design. The possibility of designing hardware which trusts the actions of the programmer is rarely considered.
In the current state of things, I find it hard to believe automated proof checking is going to advance state of programming practice, or really even make a dent of impact for that matter. If there is any value in automated proving techiniques for programming, I think it is in fully automated proofs of program properties. ML makes a strong contribution here. The pattern matching of ML ensures all clases of input are handled by he programmer. Static anaylsis of programs is large field of computer science, which has a steady stream of results. For example, things as complex as program termination have been proved automatically for large clasess of programs in Prolog. Perhaps these analyses can instill a greater sense of rigor in less skilled programers, but the larger deficit of design and problem solving skills remains unanswered.