[seb314]

> 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.

[opnitro]

In fact all major type systems work this way.