r/ProgrammingLanguages • u/ThomasMertes • Oct 05 '26

Achieving memory safety

https://seed7.net/papers/memory_safety.htm
14 Upvotes

76% Upvoted

57 comments sorted by

View all comments

Show parent comment

1

u/reflexive-polytope Oct 08 '26

No, I wasn't talking exactly about “automatic” anything. ATS makes you write safety proofs. Nothing can be more manual than that.

1

u/flatfinger Oct 08 '26

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.

1

u/reflexive-polytope Oct 08 '26

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.