This doesn't make much sense to me. Object-orientation in itself is simply another level of data abstraction. And for the rest, I think "provability" is more theoretical than practical, other than the most trivial programmes.
I'm beginning to get the impression (or perhaps more accurately am increasingly getting the impression) that the plan9 community is reactionary rather than progressive... not a good characteristic if one is trying to make advances in comparison with one's predecessors...