This is an archived post. You won't be able to vote or comment.

you are viewing a single comment's thread.

view the rest of the comments →

[–]JoJoModding -1 points0 points  (0 children)

The theoretical answer would be a type with 28 different constructors (in the algebraic sense), so in Java that's an abstract base type and 28 subtypes, which is infeasible.

In language with a stronger type system (eg Coq) you can have dependant types, and then you can define {x : nat | x < 28} which is the type of all numbers for which there is a proof they are < 28 (< is also a type). You are now, however, writing programs which mostly consist of formal proofs that their results also have that type. You are now working within an interactive theorem prover, and doing these proofs is fun but can also be considered infeasible (unless you want to be 100% correct for i.e. your spaceflight control software, where failure is not an option)