I am not in a position to tell how much more research should be done on the topic, but I can tell you that there is research being done, for example the Verisoft XT program funded by the german government.
The concepts which I think you are looking for are called formal verification and contract based programming, where the latter is a programmer-friendly way of doing the first. In contract-based programming you first write your code as normal and then insert so called contracts into the code. A readily usable language which is based on this paradigm is Spec# by Microsoft Research, and the functionally similar but slightly less pretty Code Contracts extension for C# which you can both try out online (they also have similar tools for other languages, check out rise4fun). The "int with range type" you mentioned would by reflected by two contracts in a function:
Contract.Requires(-3 <= a && a <= 24);
Contract.Requires( 3 <= b && b <= 10);
If you want to call that function, you then have to use parameters which are ensured to meet these criteria, or you get a compile time error. The above are very simple contracts, you can insert almost any assumption or requirement about variables or exeptions and their relation which you might think of and the compiler will check if every requirement is covered by either an assumption or something that can be ensured, i.e. derived from the assumptions. That is why where the name stems from: The callee makes requirements, the caller ensures that these are met - like in a business contract.
Under the hood, code contracts are usually combined with knowledge about the inner workings (operational semantics) of the programming language into a list of verification conditions. This list represents basically one big logical proposition $P(x_1,x_2,...,x_n)$ with $n$ free variables - the inputs of your program. If the proposition $P$ is true for all possible variable assignments, then the program is considered correct. To check whether or not this is the case, an SMT Prover is used. From the CS side, those two are the critical parts of the process - the generation of verification conditions is tricky and SMT is an either NP-complete or undecidable problem, depending on the considered theories. There is even a competition for SMT solvers, so there certainly goes some research into this. Additionally, there are alternative approaches to using SMT for formal verification like state space enumeration, symbolic model checking, bounded model checking and many more which are also being researched, albeit SMT is, afaik, currently the most "modern" approach.
Regarding the limits of the general idea:
- As previously stated, proving the correctness of the program is a computationally hard problem, so it might be possible that the compile time check of a program with contracts (or another form of specification) takes really long or might be even impossible. Applying heuristics which work well most of the time is the best one can do about it.
- The more you specify about your program, the higher gets the probability of having bugs in the specification itself. This can lead to false positives (the compile time check fails even though everything is bug-free) or the false impression of being safe, even though your program still has bugs.
- Writing contracts or specifications is really tedious work and most programmers are too lazy to do it. Try writing a C# program with code contracts everywhere, after a while you will think "come on, is this really necessary?". That is why formal verification is typically just used for hardware design and safety critical systems, like software controlling airplanes or automotives.
One last thing worth mentioning which does not quite fit the above explanation is a field called "Implicit Complexity Theory", for example this paper. It aims at characterizing programing languages in which each program you can write falls into a specific complexity class, for example P. In such a language, each program you write is automatically "ensured" to be of polynomial runtime, which can be "checked" at compile time by simply compiling the program. I do not know of any practically usable results of this research, however, but I am also far from being an expert.
dependent type
orrefinement type
. $\endgroup$