i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1]
> I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technology does not promise, however, to save labor. Verifications are so much work that only a few substantial programs have ever been verified
[1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p...:
> I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technology does not promise, however, to save labor. Verifications are so much work that only a few substantial programs have ever been verified