Category: proof

Formal methods have been popping up in the news again, or at least on the technical news sites I follow. Both mathematics and software share the same pattern of usage of formal methods. The input text is mapped to some output text. Various characteristics of the output text are checked using proof assistant(s). Assuming the…