| ▲ | zozbot234 2 hours ago | |
Proofs of safety are proving a negative: they're all about what an algorithm won't do. So constructivism is irrelevant to those, because the algorithm has provided all the constructive content already! Proofs of liveness/termination are the interesting case. You might also add designing an algorithm to begin with, or porting it from a less restrictive to a more restrictive model of computation, as kinds of proofs in CS that are closely aligned to what we'd call constructive. | ||