You are right, and I think you've found one of the weak spots. But I do think that can be treated, and the advantages of the programming-ease will be a good tra

You are right, and I think you've found one of the weak spots. But I do think that can be treated, and the advantages of the programming-ease will be a good trade-off in many cases with the lost control for efficiency. It's like the switch from assembly to C, or from manual memory management to automatic memory management. You lose something. You gain something else. The new approach is not valid for everything, but for some/many cases, it's much better. Yes, the spec of a complete program will still be a great amount of work. The default resulting code will probably be slow. But you will be able to "describe" the program (in many cases), and you will be able to optimize it later without risking the correctness. Hopefully that can be a great aid and tool in many cases. We'll see, and I hope to have a lot of help along the way doing it publicly! BTW, if what comes out is just a good new approach to static code analysis / formal specification / etc... it will have been worth it. But I do hope to find a usable tool at the end of this quest :)