> High level application development might not change that much since the problems are usually poorly specified. But it might dramatically reduce the cost of wr

> High level application development might not change that much since the problems are usually poorly specified. But it might dramatically reduce the cost of writing system software. I don't see that specifying system software is any easier - getting a specification in machine format is surely more-or-less equivalent to writing the program, and the specification is likely to not encode every single desire correctly - i.e. the spec will have bugs? Or, in other words - you might not be proving what you think you're proving. You're proving what the code says you're proving, which is an entirely different thing.