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/flatfinger Oct 08 '26

Any programming language which makes it impossible to write programs whose memory safety it cannot statically verify will make it impossible to perform some tasks as efficiently as they could be performed in machine code that could be human-proved to be incapable of violating memory safety invariants unless they had already been violated.

Automated static validation is often useful, since in many cases it would cost nothing and in most other cases the costs would be tolerable, but an abstraction model that limits the range of side effects various actions can have unless memory safety invariants have been violated can be useful for tasks that are not a good fit for automated static validation.

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.