I'm interested in proofs using ideas from outside commutative algebra of Hilbert's Basis Theorem.
If $R$ is a noetherian ring, then so is $R[X]$.
or its sister version
If $R$ is a noetherian ring, then so is $R[[X]]$.
I am very much aware of the standard non-construtive proof by contradiction given by Hilbert as well as the direct version using Groebner basis.
Most important theorems in mathematics that are old enough have several very different proofs. Comparing different ideas can be very enlightening and also give a hint to possible generalizations in different areas. For the Basis Theorem however, I am not aware of such.
Best Answer
Sorry, this is not an answer, but rather a too-long elaboration on constructive aspects. I post this here because there was some interest about the constructive content of the theorem in the comments.
As pointed out in the comments, the first thing to get straight is the definition of a Noetherian module (or ring). For instance, with the usual definition "any submodule is finitely generated", even the $\mathbb{Z}$-module $\mathbb{Z}$ cannot be shown to be Noetherian constructively: Pick a formula $\varphi$ such that neither $\varphi$ nor $\neg\varphi$ can be shown. Then consider the submodule $U = \{ x \in \mathbb{Z} \,|\, (x = 0) \vee \varphi \}$. If $U$ were finitely generated, it would a forteriori be generated by a single element (Euclid's algorithm) and we could decide whether $1 \in U$ or $1 \not\in U$, that is whether $\varphi$ or $\neg\varphi$.
A suitable notion of a Noetherian module is given in the very fine book A Course in Constructive Algebra by Mines, Richman, and Ruitenburg: A module is Noetherian if every ascending chain of finitely generated submodules stops (think "$U_n = U_{n+1}$", not "$U_n = U_{n+1} = U_{n+2} = \cdots$").
This definition works fine for many purposes, but not for showing that $R[X]$ is Noetherian if $R$ is. See Chapter VIII of that book. Also it doesn't work well if dependent choice is not available, since it refers to sequences, which can be quite elusive without choice.
A different definition appears in http://www.mittag-leffler.se/sites/default/files/IML-0001-30.pdf (by Coquand and Lombardi). There they claim that Noetherianity of $R$ implies Noetherianity of $R[X]$.
Finally let me recommend the nice article Strongly Noetherian rings and constructive ideal theory by Hervé Perdry. He surveys several kinds of Noetherian conditions.
A thesis of Coquand, Lombardi and others is that the Noetherian condition is often not the right one constructively. Instead, one should refer to the notion of a coherent ring. In classical mathematics, any Noetherian ring is coherent. See for instance page 27 of Commutative Algebra: Constructive Methods by Lombardi and Quitté.
Finally, a short and constructive proof that the Krull dimension of $K[X_1,\ldots,X_n]$ is $n$ appears at http://hlombardi.free.fr/publis/KrullMathMonth.pdf (by Coquand and Lombardi).