Ada cannot do this at compile time. Predicates with arbitrary logic like that are checked with runtime assertions. There are limits on which static predicates y

Ada cannot do this at compile time. Predicates with arbitrary logic like that are checked with runtime assertions. There are limits on which static predicates you can write. F* implements refinement and dependent types, which allow true logic to be computed at _compile_ time.