Both your examples (is my number prime, are my XML nodes unique) are easily expressed in a dependently-typed language.
Dependent type checkers may be hard to implement, but the typing rules are fairly simple, and people have been using this correct by construction philosophy using dependently-typed languages for a while now.
Dependent type checkers may be hard to implement, but the typing rules are fairly simple, and people have been using this correct by construction philosophy using dependently-typed languages for a while now.
There's nothing delusional about that.