For this type of question the first reference that comes to my mind is P.T.Johnstone Sketches of an elephant, part C.
Most of the results in this book are constructively valid: If a result is proved over an arbitrary base (either a topos or a locale), it means that it is constructive, the few non-constructive result present in the book are those that explicit refers to the category "Set".
To answer your more specific questions:
- One says that a locale is discrete if its diagonal map is open and if the map $X \rightarrow 1$ is open (the second condition is automatic in classical mathematics, but not in constructive mathematics). With this modification they are the standard definition (at least equivalent to them, we generally don't invoke the Sierpinski locale to define what are open and closed subsets, they just corresponds to the element sof the defining frame).
The only things you might want to be carefull about is that for a spatial locale, being Hausdorff in this sense is not exactly equivalence to the fact that the corresponding topological space is not Hausdroff, but this is already the case in constructive mathematics.
A locale is discrete in your sense if and only if it is the frame of subset of a set. (Lemma C3.1.15 of sketches of an elephant). The set is decidable if and only if the locale is Hausdorff.
Because of point $(2)$ one has that:
Discrete => spatial
and "Discrete => Hausdroff" is essentially equivalent to the law of excluded middle.
But there is no other implications: boolean locales are Hausdorff but not spatial nor discrete, and spatial locale can be both discrete and non discrete and both Hausdorff and non Hausdorff.
This being said, there is one more important implication:
If $X$ is spatial then the map $X \rightarrow 1$ is open (C3.1.16 in sketches). So with your defition of discrete what is true is that $X$ corresponds to a set if and only if $X$ is discrete and spatial.