Should Your Specification Language Be Typed

• Main example: is $i-j<0\to A[i-j]=A[i-j]$ bogus for an array $A:\mathbb{N}\to\alpha$.

• Deep confusion about subtyping: should be handled by elaboration. Mostly a product of the 90s.

• Very misleading/incorrect statements about dependent type theory:

  Since most computer scientists do prefer classical reasoning, constructive type theories are not widely used.

  This is just incorrect.

• Deep confusion about things like $1/0$.

• First-order logic is simply not enough for software specification; anything with induction schemas is absolutely horrible.

• Set theory is unityped, not untyped