Formalism in integration Let's say we have some $y(t)$. The derivative of $y$ along time axis will be $y'(t)=\frac{dy(t)}{dt}=\frac{dy}{dt}$. So I will integrate like this over time:
$\require{cancel}$
$\int_{t=0}^{+\infty}\frac{dy}{\cancel{d\tau}}\cancel{d\tau} = \int_{t=0}^{+\infty}dy=y|_{t=0}^{+\infty}=y(\infty)-y(0)$ , (since $y = y(t)$)
Even though the result being correct, is this procedure correct according to formalism?
In other words:


*

*can I cancel the differentials? Thinking of interval that makes sense to me.

*can the integral variable be different from the differential (second step)? I've almost never see the integration variable explicitly shown like I put there.

*I solved the integral in the third step as my variable was $y$ even though it was actually $\tau$. Can that be done?

 A: We chose the fraction-looking notation for derivatives because many "apparent laws", like this cancellation, really do hold. But the notation alone is not a proof of this.
This question is really a question about what many call "u-substition" in disguise. u-substitution is an integral statement of the chain rule for differentiation, and this is why you can "cancel the $\mathrm{d}\tau$ terms." For a proof that this works, you might look up proofs of u-substition. I happen to have written a proof in another answer, and in that answer the equality that you want is colored in red (suggesting that this is a common source of confusion).
The bounds of integration are treated exactly as you have treated them. 
When you ask about integrating with respect to $y$ "even though it was actually $\tau$," you are in fact integrating against $y$. This is the same question as your first question, and the proof is also contained in the other answer. 
In general, we have that
$$ \int_a^b f(g(x))g'(x)\mathrm{d}x = \int_{g(a)}^{g(b)} f(y)\mathrm{d}y,$$
for sufficiently nice $f,g$.
A: Since you are asking about being formal, many would insist on using limits when doing an improper integral:
$$
\int_a^\infty y(t) \; dt = \lim_{K \to \infty}\int_{a}^K y(t)\; dt.
$$
Note that $y(\infty)$ doesn't (formally) make sense unless you have a function where $\infty$ is an element in the domain.
I would also say that by writing:
$$
\frac{dy}{\cancel{d\tau}}\cancel{d\tau}$$
you are implicitly saying that the derivative is a fraction and many would object to this (in particular in a basic calculus class). I, by the way, assume that $\tau$ is the same as $t$ in your example. Otherwise there is something that I don't understand.
A: The biggest problem with your work is that you use the unfortunate convention to use $y$ both as a variable, and also for the function relating $y$ to $t$.
I will introduce the letter $f$ for that function; that is, $y$ is related to $t$ by the equation $y = f(t)$.
You can't cancel the differentials in the sense of combining everything into a single fraction cancelling like terms out of the numerator and denominator. However, it is true (in single-variable calculus) that
$$ \frac{dy}{dx} \, dx = dy \qquad \qquad \frac{dy}{dx} \frac{dz}{dw} = \frac{dy}{dw} \frac{dz}{dx} $$
so you can do things that look very much like what you can do with fractions, even if you can't treat them as actually being fractions.
In multivariable calculus, for most pairs of differentials, you can't write one as a multiple of the other, so ratios like $\frac{dy}{dx}$ are nonsensical unless you happen to know $y$ and $x$ are related by a differentiable function. Partial derivatives, e.g. $\frac{\partial y}{\partial x}$, have a lot of subtle issues and shouldn't really be treated like ratios at all.
When you're using notation involving variables like $y$, rather than one using functions like $f$, integrals are often better thought as integrating over a path rather than between two numbers. It's not usually introduced that way, however, since it would make definitions somewhat more complicated.
At one endpoint of the path, you have $t=0$ and $y = f(0)$, and at the other endpoint, you have $t=+\infty$ and $y = f(+\infty)$. It doesn't really matter which letter you use in an expression as the 'variable' for the path integral, since the path 'remembers' what all the variables should be. But, of course, if you don't use notation reminding yourself that you're thinking of a path, you can get into trouble. (e.g. you could easily forget half-way through and think you've written numbers that are the values of the variable you're currently using)
Finally, you should take care to remember that this is an improper integral: it really should be computed as a limit of proper integrals. I'm not sure if any of the ideas I've described here run into problems when you try to use them in an improper integral.
