According to the definition of safety property, a property like "The program shall never trap/crash" is a safety property. This is a property that is frequently not uphold in "safe languages".
The definition of X safe operation nicely avoids this pitfall, by not mentioning how the safety property X is uphold:
An X safe operation upholds some safety property X even if preconditions are violated.
But, later on the definition of safe operation (and implicitly safe language), mention trapping as a way to construct safe operations:
“Trapping” or otherwise stopping the program when preconditions are violated is one way to achieve safety.
Trapping is not a good strategy for programs in which "no-trapping" is a safety property.
I would suggest slightly altering the phrase about trapping to indicate that this is just a strategy and may not work in the case of no-trapping safety property. Maybe adding a footnote is enough.
Similarly, I would point out (probably in a footnote) that safe languages are, by design, not upholding the no-trapping safety property.
According to the definition of safety property, a property like "The program shall never trap/crash" is a safety property. This is a property that is frequently not uphold in "safe languages".
The definition of X safe operation nicely avoids this pitfall, by not mentioning how the safety property X is uphold:
But, later on the definition of safe operation (and implicitly safe language), mention trapping as a way to construct safe operations:
Trapping is not a good strategy for programs in which "no-trapping" is a safety property.
I would suggest slightly altering the phrase about trapping to indicate that this is just a strategy and may not work in the case of no-trapping safety property. Maybe adding a footnote is enough.
Similarly, I would point out (probably in a footnote) that safe languages are, by design, not upholding the no-trapping safety property.