Programming Languages - What You Mean by Undecidability?

verification is a very shiny and attractive goal, because there's this basic fact about programming: we're all terrible at ity. But the idea of specifying these properties on the side somewhere, or even in the program, but any different syndex, i think it's a big problem for adopting this kind of technologies. It's possible to specify something about the library, but keeping it up to date as the code evolves is very hard. When you try to reason about it, and you have a tool that runs together with the code, takes the specification and the code and checks them against each other as you do the development. There is some hope to keep the cod and the speck al