> And are you saying formal proof assistants like coq and isabelle are fools errands[?] No, and I have no clue how you could get that from what I wrote. To mov

> And are you saying formal proof assistants like coq and isabelle are fools errands[?] No, and I have no clue how you could get that from what I wrote. To move back into a more familiar domain, Rice's theorem puts a frustrating limit on what we can accomplish via static analysis of programs, and yet the static analysis we can do remains extremely helpful in programming.