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.)
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.)