I would disagree on a few counts.
I don't think it's "probably" possible to prove $P \neq NP$. I certainly don't think it's impossible, but Gödel's incompleteness theorems tell us that there are some sentences in a logical system which are true but which can't be proven.
You ask if there have been proofs to Computer Science theories. There have been thousands at the very least. These vary from insignificant to huge. I'll mention some of the most relevant (aka my favorite) ones here.
- Some problems cannot be solved by ANY algorithm. No matter what. Ever. An example of this is determining if a computer program will run forever. There is no way to look at a program and be guaranteed a yes/no answer for if it will run forever.
- The functions which can be computed by a Turing Machine are the same as functions which can be computed by the lambda calculus, are the same as practically every programming language. Basically, though speed might differ, all turing-complete programming languages (which is most of them) can solve the same set of problems.
- The types of a computer program are directly related to its proof of correctness. This is called the "Curry-Howard Correspondence", and is quite complex, so I won't go into the details here. Note that by types I mean things like integer, string, list, array, etc.
- A list of real numbers can't be sorted in faster than $\Omega (n\log n).$ This means that no matter what algorithm you use, in the worst case it will take approximately $n\log n$ steps to sort that list.
- A large number of problems are, at their core, the same problem. If you've ever heard of NP-complete problems, what that means is that these problems all boil down to satisfiability. They are from graph theory, combinatorics, scheduling, and a variety of areas, but ultimately, they are all just checking if there's some input to a logical formula of ORs and ANDs which will spit out true as the overall result.
Note that these are all necessarily complex topics, which I have simplified to give you a taste of the sort of things provable in computer science.
You ask how Computer Science theories are proven. The problem is that Computer Science is an incredibly diverse field, and it really depends on your sub-field. Theory of computation, programming language construction and formal AI ("neat" AI) are highly mathematical, and are based heavily on logic and proofs.
However, there are many sub-fields which are much more experimental. Human-Computer interaction or anything having to do with the human side of computing will rely heavily on studies and experiments involving users. Operating Systems, Graphics and Compilers will rely heavy on performance evaluations, seeing which programs are fastest in the real word, not just on paper.
If you are in Junior High, I think there are many computer science problems which are in your reach. Because it is such a young field, there are many unsolved CS problems which are relatively simple to understand. Unlike physics, where you need tons and tons of calculus background, CS really relies on simple logic. If you can learn induction, logic and the basics of discrete structures (graphs, strings, etc.), I think there are probably lots of concepts that are accessible to a Junior High student.