What formal properties should resolution of singularities have? If I were going to propose a new construction as a "replacement for resolution of singularities", what properties would my replacement have to have?  [I am going to do no such thing -- this is purely speculative.] Is there a shortish list of theorems such that any construction verifying the properties on the list would thereby deserve to be called a resolution of singularities?  
 A: 
It should exist in all characteristics, even mixed characteristic! 

This sounds somewhat cheeky, but I was fairly serious. To algebraists, and the OP is one last time I met him, a purely ring-theoretic statement which can largely only be verified in char. $0$ feels more incomplete than to a geometer. 
This is a main reason why the use of resolution of singularity is restricted in attacking some of the open questions in commutative algebra: often the hardest case is mixed characteristic, and if you are extremely lucky and smart you can reduce it to a statement in char. $p>0$, then you are dead!
Because of the above reason, I would mention that de Jong's alteration  has found some spectacular success in commutative algebra (so one can  replace birational by surjective and generically finite). A main example is Gabber's proof of the non-negativity part of Serre's conjectures on intersection multiplicities (see number 1 here for an expository account) .  
A: I'm guessing quite a few users would want the resolution construction to be equivariant.
A: Here are some properties of resolution of singularities that I use often:


*

*The map is an isomorphism (or some version of very nice) over the smooth locus is important.   EDIT:  This usually shows up because I want to make statements about properties of the singular locus itself.  One common application of this is that any smooth variety can be embedded in a smooth complete variety (do any embedding, and then resolve the singularities).  A sufficiently good version of (3.) also should imply this (ie, if the resolution procedure commutes with open immersions).

*The pre-image of the singular locus (or some specified subscheme) is SNC, aka simple normal crossings (or at least something very well understood). EDIT:  Two is used for vanishing theorems certainly, but it also tells you in many cases when you can stop.  Sometimes, especially when you are given a specific subscheme $Z \subseteq X$, the data the resolution provides without the SNC hypothesis is incomplete, but after one does further blowing up and arrives SNC case, no new data can be obtained by further resolution.  Also, the embedding statement from (1.) then becomes ``you can embed any smooth variety in a smooth complete variety where the boundary divisor is a SNC divisor''.

*Some version of functoriality is important.  EDIT:  There is of course the formal versions of functoriality out there (ie, compatibility with smooth maps, various equivariant forms, etc...)  There are also important implicit forms too.  Often you have a map of varieties and you need to have resolutions of their singularities that also have a map between them.  In this case, you usually can't use functorial resolutions on both, but after you do one, you can often then know what has to be done in the other (ie, resolve the singularities of one, then resolve the indeterminacies of the map, then resolve the singularities of the other).  Sometimes the fact that resolutions can be described by blow-ups helps in this context.
A: It seems to be important that the resolution of singularities be a proper map.
