Well, most interesting properties about computer programs are, in general for all programs, undecidable (https://en.wikipedia.org/wiki/Rice%27s_theorem). Undecidability is a closely related notion to unprovability (https://en.wikipedia.org/wiki/Undecidable_problem#Relationsh....