Verification

I see a lot of programming work with statements like ( by redoing software like this it would be possible to do formal things with it ) . For example functional programming languages make this big claim that using this you could make something 'provable'.

This is the first time I've every seen something actually proved and its of some use. I think the next thing they should attempt is a garbage collector. I wonder how they handled multi-threading ( I guess that's what took 6 years )