What's not rigorous about antidifferentiation being integration? You can prove it same as any other theorem.

As my teacher used to say in 6th form:

"Ya do Dee Why by Dee Ex and, eef ya theenk aboot it, you get Dee Why by Dee Ex Squared"

gmk2 wrote:Is there any way of looking at integration other than it simply being differentiation backwards?

Yes, integration can be defined completely independently of differentiation. I can think of situations where a generalised concept of integral is applicable and derivative probably isn't, and vice versa.

Can you derive a formula for integration from first principles in the same way you can for differentiation?

If by "formula for differentiation", you mean lim[(f(x)-f(y))/(x-y)] as y->x, there are formulae like that for integrals. If you only need to integrate nice functions like continuous functions you can keep it quite simple and it lets you calculate the value of an integral to arbitrary precision as long as you can calculate the values of the function. As you work with nastier and nastier functions the simple definitions break down and you have to use more convoluted definitions (there are lots of ways of doing it), and a formula expressing it will become an impractical messy pile of symbols. The highly abstract definitions need to be used in contexts where nice formulae for things are a great luxury anyway, and you will probably not have any way of calculating the actual values of the function, you just know it has certain properties and you want to know what else you can say about it.

If you mean you have a formula defining a function in terms of certain other functions like sin and log that you regard as especially friendly, and you want to turn it into an exact formula for an antiderivative of it, this is usually much more difficult than for derivatives, and can be impossible even with quite friendly formulae, though surprisingly, it apparently is always possible to decide when it is doable with the so-called "elementary" functions and to do it when you can. This is not really important for understanding what integration actually is though. I've never understood why people fixate on those functions anyway.

I don't strictly need to know, but looking at it as simply doing differentiation backwards doesn't seem very rigourous

Once you properly define integrals, you can rigourously prove their relation to antiderivatives.

I prefer to try and understand concepts as deeply as I can.

Afaik, at the deepest level integration is a way that linear functionals arise naturally from measures. If you are just starting to learn about integrals you are probably not in a position to understand this.