> However, it seems that there is a tremendous amount of effort that goes into proving this software and I wonder if the time investment makes sense.
I suppose the effort wasn't just to prove this software correct, but to develop a methodology that allows proving other similar software.
> I wonder whether it will ever be feasible to make this part of everyday software development
I think that's where we're headed. For one thing, verification could be much easier with a language that was designed to ease verification (not C!).
We can also expect to eventually have a lot of proved correct components that we'll glue together using some languages that makes it easy to prove that the composition is correct.
I suppose the effort wasn't just to prove this software correct, but to develop a methodology that allows proving other similar software.
> I wonder whether it will ever be feasible to make this part of everyday software development
I think that's where we're headed. For one thing, verification could be much easier with a language that was designed to ease verification (not C!).
We can also expect to eventually have a lot of proved correct components that we'll glue together using some languages that makes it easy to prove that the composition is correct.