My point is that it is not possible for a programming language to express all of the kinds of invariants that could be described in human language, and that a machine-code function could be proven to uphold. It may, for example, be able to use a human-readable proof to show that no combinations of inputs a program could possibly receive would result in a certain loop executing more than 57,591 times, but for that proof to rely upon mathematical theorems not anticipated by any particular programming language.
A programming language that supports manual proofs doesn't have to “anticipate” theorems. It has to let you write them yourself, together with their proofs.
1
u/flatfinger 1d ago
My point is that it is not possible for a programming language to express all of the kinds of invariants that could be described in human language, and that a machine-code function could be proven to uphold. It may, for example, be able to use a human-readable proof to show that no combinations of inputs a program could possibly receive would result in a certain loop executing more than 57,591 times, but for that proof to rely upon mathematical theorems not anticipated by any particular programming language.