i.e. even in strongly typed languages the type-checker can tell you at compile-time if the function will output an int but cannot guarantee that the int will be < 9000 and I think something like the latter is the kind of guarantee we need for alignment
Define a new type that only allows ints < 9000 if needed?
For your broader question, I think there might be some safety relevant properties of some alignment primitives.
Beren, have you heard of dependent types, which are used in Coq, Agda, and Lean? (I don’t mean to be flippant; your parenthetical just gives the impression that you hadn’t come across them, because they can easily enforce integer bounds, for instance.)
Define a new type that only allows ints < 9000 if needed?
For your broader question, I think there might be some safety relevant properties of some alignment primitives.
Beren, have you heard of dependent types, which are used in Coq, Agda, and Lean? (I don’t mean to be flippant; your parenthetical just gives the impression that you hadn’t come across them, because they can easily enforce integer bounds, for instance.)