4 ms·
I think being able to prove that a program can be correct is getting close to P=NP territory.
by Dirlewanger 6y ago
I think being able to prove that a program can be correct is getting close to P=NP territory.
- Raptor22 6y agoIt's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....
- aklein 6y agoCannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.