I am sorry, I am not a real computer scientist and I find it difficult to find the right term. With "sufficiently expressive", I mean things like dependent types and refinement types, that can express the constraint on a unit vector.

It seems to me that this is more or less the same thing, but Monte Carlo. Like MCMC vs symbolic Bayesian inference.