> The branching factor in the proof search is essentially infinite so you cannot just do an exhaustive search. That was the impractical part. Exhaustive searc

> The branching factor in the proof search is essentially infinite so you cannot just do an exhaustive search. That was the impractical part. Exhaustive search scales so poorly it can't be seriously considered. > That proof will be fairly easy because the algorithm, data structure and the program property definitions will all have a similar shape which won't be the case for e.g. quicksort or heapsort. I would agree that heapsort (using an array/list for the heap) would be much harder to prove, but I would expect quicksort to be fairly similar (probably a bit harder). > Keep going with your idea, I just mean to be aware that you're hitting against problems that are well known to be very difficult, have lots of existing related work and are still current research areas. Coq etc. are a long way from being mainstream because of this. Yeah, I never planned to push research forward with the idea. Primarily, I would like to explore it just to improve my own knowledge; its much easier to know why something is hard once you've failed at it yourself. And perhaps make an interesting toy language.