Perhaps this is not an appropriate question for MO, but having just discovered this site I wanted to ask it.
Is there a rigorous definition as to what "a quantization" of a Hamiltonian dynamical system actually is? I have never been satisfied with the answers my physicist friends have told me. The kind of answer I have in mind is something "a right inverse to the map which sends a $\Psi$DO to its principal symbol".