But the abstract structure of quantum algorithms is all about the carefully orchestrated structure within entanglement, not whether entanglement is present. Also, even just considering whether entanglement is present, the rules that they use in the language are far too weak. They basically amount to "if you do a two qubit operation it might be entangled". How is something like that ever going to help verify, for example, that already-allocated-but-currently-unused qubits being used as dirty ancillae (as in [1]) are being correctly restored (e.g. disentangled from the context where they were temporarily used)? It's just going to say "I dunno, they touched, they might be entangled". But I know they touched and might be entangled. I'm looking for a more gradual transition from "I applied no operations therefore everything is fine" to "I need to spin up a Turing complete simulator and do runtime analysis".

> if teleportation was "built-in" for the language, then the language would be useless for anything but "numerics"

I didn't mean to suggest hard-coding teleportation. What I was picturing is that the language would understand the stabilizer formalism [2], which is powerful enough to encode many quantum protocols but restricted enough to guarantee efficient classical analysis. Teleportation is a special case of things efficiently handled by the stabilizer formalism.

1: https://arxiv.org/abs/1611.07995

2: https://arxiv.org/abs/quant-ph/9705052

I would love if someone could make a type system that gave me similar benefits and scaled to complete algorithms. But a verbose system for keeping track of who-touched-who just isn't it.

1: https://quantum-journal.org/papers/q-2021-07-06-497/ or https://github.com/quantumlib/Stim/

Hey, when everyone else is falling back to "oh we just simulate the hard cases to verify them", making simulation faster is making verification better.