I agree with 1 but:
> 2. When there's some large set of instances of some NP-hard problem that are tractably solvable in practice (like SAT), the importance of that is that there's some non-NP-hard subset here. Indeed, SAT is FPT (fixed parameter tractable [1]), an "easier" type of NP, for which decomposition can help. In contrast, graph colouring is thought to not be FPT.
Sorry but I need to clarify here. "SAT is FPT" does not mean anything. FPT only makes sense when you tell what is the *parameter*. Every problem is FPT when parametrized by the input size so graph colouring and SAT are FPT wrt to the size of the input (the graph and the formula respectively). What you meant: graph colouring parametrized by the number of colours is unlikely to be FPT (since it is W[1]-hard). SAT is FPT for many parameters such as treewidth (of the formula). Oh, and btw, graph colouring is also FPT when parametrized by treewidth (of the graph).
I take your correction re graph colouring, but the rest is pointlessly pedantic (especially "FPT in the length", which is trivial and so typically excluded from the definition).
Now, I don't know if SAT being FPT (in a parameter of interest) has anything to do with the surprising ease of many "natural" instances (even with many variables), but my point was that when many instances are easy, that doesn't mean that the class is irrelevant, it just means it's more interesting (as there's obviously a tractable subclass, albeit one we haven't yet defined succinctly).
Late answer but I need to be pointlessly pedantic again, because it is apparently what it is called to correct something that does not make sense. That said, I agree with your way of reformulating your point.
To first address the pedanticness: "FPT in the length of the input" is not excluded from the definition of FPT even if it is not an interesting case. Excluding these cases from the definition would make the theory uselessly complicated.
Now, back to the point of my first comment. It was mostly to show that you cannot use "FPTness" as an argument to justify that SAT is "easier" than graph colouring. I used "length of the input" to give an easy counter example, to show that FPT is not "an easier type of NP". It never has been. It is a way of understanding and measuring the complexity of the problem finely, to isolate hard parts of the input from the rest. What the W[1]-hardness of graph colouring parametrised by the number of colours tells you is that this parameter is not a relevant parameter and that's it. Graph colouring is FPT for many relevant graph parameters such as treewidth, clique-width (SAT is not even FPT wrt clique-width, but again, you cannot really use the concept of FPT to compare problems).
You will have a hard time using theory to justify that SAT is easier than any other NP-complete problem, because from the theory point of view, it is the hardest NP-problem you can get. Unless something unexpected happens in complexity theory, SAT cannot be efficiently solved in randomized time, SAT cannot be solved in sub-exponential time, SAT is complete under parsimonious reductions so you can basically take any NP-complete problem and build a CNF formula whose models are isomorphic to the solutions of the original instance etc.
The success of SAT solvers does not mean that SAT is easier than other NP-hard problem. It means that many combinatorial problems we need to solve in practice are "simple enough" that using the incredibly optimized smart way of bruteforcing the solution with a CDCL SAT solver is good enough. Now, take a cryptographic instance, translate it into a CNF formula and call a SAT solver, I doubt it will shine. Despite many attempts, this behaviour has never clearly be explained by the fact that the complexity of CDCL is FPT wrt a parameter that is small in industrial instances.
> You will have a hard time using theory to justify that SAT is easier than any other NP-complete problem
"Easier" perhaps isn't the right word (in terms of reducibility, it certainly isn't), but FPT is just a way to demonstrate that NP-complete problems can be different from each other in ways that matter (with respect to "natural" instances).
> Now, take a cryptographic instance, translate it into a CNF formula and call a SAT solver, I doubt it will shine.
Exactly. And researchers are very much interested in these differences that arise in natural instances and are hidden by "crude" reduction.