> Such compiler would require solving halting problem. I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs

> Such compiler would require solving halting problem. I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs no proof if found even though they fulfill the specification) Occasional false-negatives seem perfectly fine for real-world use.