I'm pretty far out of my area of expertise, so I'll take your word for it. Could an an algorithm be correct, but not proven correct, or is it defined as a heuristic at that point?
Pretty much everything programmers do is create unproven algorithms. Hopefully at least some of them are correct. A heuristic is a problem-solving approach that has a chance of failure. So say you need a pretty fast dictionary, and you can take a relaxed attitude to correctness. You can take a hash of the words of your dictionary, and then as you are filtering some dataset, you can always say in a short time whether a value is definitely not in your dictionary, but your positive solutions have a percent chance of being incorrect (e.g. a hash collision). The idea is generally to make a problem tractable that would otherwise be computationally difficult or impossible. I'm not sure if that quite answers your question.
An algorithm could certainly be correct (in the sense of always giving the correct result) without being proven to do so (or even without any such proof existing, in some particular formal system). You are not wrong about that.