Alright, I think I've got a proof of compactness being equivalent to sequential compactness (all countable sequences have a convergent subsequence with a limit point in the set). It relies on a series of reductions to easier and easier proof targets, until we get to something we can actually prove.
First, definitions.
A set $A$ is countably relatively compact if, given any sequence in it, that sequence has a cluster point (which may or may not be in $A$)
A set $A$ is sequentially compact if, given any sequence in it, there's a subsequence that converges to a point that lies in $A$
A set $A$ is compact if, given any open cover of it, there's a finite subcover.
A space is angelic if $A$ being countably relatively compact implies that $\overline{A}$ (topological closure) is compact, and that all points in $\overline{A}$ have a sequence from $A$ that limits to them.
Reduction step 1:
From Weakly Compact Sets by Klaus Floret, on page 40, there's a theorem that in angelic spaces, sequential compactness = compactness. That's exactly what we're going for, so our proof goal shifts to showing that $C_B(X)$ is angelic.
Reduction Step 2:
From Weakly Compact Sets by Klaus Floret, on page 40, there's a theorem that, if $\phi:Y\to Z$ is a continuous injection, and $Y$ is a regular space, and $Z$ is angelic, then $Y$ is angelic. In particular, we'll be letting $Y$ be $C_B(X)$ with the strict topology, and $Z$ being $C_B(X)$ with the weak topology, and $\phi$ being the identity function. It's clearly an injection, and continuous because the weak topology has fewer opens than the strict topology.
Thus, our proof goal shifts to showing that $C_B(X)$ with the weak topology is an angelic space, and that $C_B(X)$ with the strict topology is a regular space.
Reduction Step 3:
From Corollary 1.11.iii in "On Compactness in Locally Convex Spaces" by B. Cascales and J. Orihuela, $C_B(X,\mathbb{R})$ with the weak topology induced by the strict topology is an angelic space, as long as $X$ has a dense K-analytic subset, and $\mathbb{R}$ is in their specified class of nicely-behaved locally convex vector spaces. The latter holds because they were bragging about how large their class of vector spaces was, and $\mathbb{R}$ is, in a sense, the nicest-behaved vector space there is, so if their stunningly general class of vector spaces doesn't include $\mathbb{R}$, something has gone horribly wrong.
So, anyways, we've reduced the problem to showing that $C_B(X)$ with the strict topology is a regular space, and that $X$ has a dense K-analytic subset.
Reduction Step 4:
From "Compact Coverings for Baire Locally Convex Spaces" by J Kakol and M Lopez Pellicer, in the introduction, $X$ being analytic implies it's K-analytic, and a space $X$ is analytic if there's a continuous surjection $\mathbb{N}^{\mathbb{N}}\to X$. Also, by the Wikipedia article for Baire Space (set theory), every Polish space $X$ fulfills that property. Our space is Polish, so by this argument, the entire space $X$ counts as a dense K-analytic subset of $X$.
The problem has now been reduced to just showing that $C_B(X)$ with the strict topology is a regular space.
Reduction Step 5:
We'll prove that if $C_B(X)$ with the strict topology has the following property, it's regular. The relevant property is...
There's a local basis of the constant-0 function consisting of open sets, $\mathbb{B}$, where, for every $U\in\mathbb{B}$, there's a open set $U'$ s.t. $0\in U'\subseteq U$, and for all $f\not\in U$, there's an open neighborhood of $f$ that's disjoint from $U'$. (strict topology used throughout)
Assume this property holds. Then, given any point $f$ and closed set $C$ with $f\not\in C$, we can generate disjoint open neighborhoods of $f$ and $C$ (establishing that $C_B(X)$ is normal), as follows. $C^c$ is an open that contains $f$. Thus, $C^c-f$ (shifting our open set) is an open neighborhood of 0. Then, we can pick a smaller open from the local basis of 0, call it $U$. Then, we generate the indicated set $U'$ from our assumption. And now, $U'+f$ and $(\overline{U'}+f)^{c}$ will act as our disjoint open neighborhoods for the point $f$ and closed set $C$, respectively.
Verifying openness and disjointness is pretty easy, as is verifying that $f\in U'+f$, because $U'$ was an open neighborhood of 0. Establishing that $C\subseteq(\overline{U'}+f)^{c}$ is more difficult. We'll do this by showing that $\overline{U'}\subseteq U$, because if we can show that, then it'd mean that $\overline{U'}+f\subseteq U+f\subseteq(C^c-f)+f=C^c$ (remember, $U$ was selected to be an open subset of $C^c-f$). And then, from that, it means that $\overline{U'}+f\cap C^c=\emptyset$, and from there, that $C\subseteq(\overline{U'}+f)^c$, which is what we wanted to show.
That just leaves showing that $\overline{U'}\subseteq U$, which can be done, because by our starting assumption, all the $f\not\in U$ have an open neighborhood $U_f$ that doesn't intersect $U'$, which witnesses that $f$ is not included in the intersection of closed neighborhoods of $U'$. Thus, the closure of $U'$ can't include anything from outside of $U$, and everything works, we've proven that $C_B(X)$ with the strict topology is normal.
And so, all that remains is just proving that assumption, that there's a local basis of the constant-0 function consisting of open sets, $\mathbb{B}$, where, for every $U\in\mathbb{B}$, there's a open set $U'$ s.t. $0\in U'\subseteq U$, and for all $f\not\in U$, there's an open neighborhood of $f$ that's disjoint from $U'$.
Reduction Step 6:
Actually proving that damn thing. We'll be using Theorem 2.4a from Bounded Continuous Functions on a Completely Regular Space, by F Dennis Sentilles, that explicitly gives a local basis. It is as follows. It's parametrized by a family $\{K_n,a_n\}_{n\in\mathbb{N}}$, where the $K_n$ are compact subsets of the space $X$, and $a_n$ are a sequence of numbers s.t. $\min_{n}a_n>0$ and $\liminf_{n\to\infty}a_n=\infty$. The open set corresponding to a family like that is
$$\{f|\forall n:f(K_n)\subseteq(-a_n,a_n)\}$$
These fulfill the property to be a strict-open, that, when restricted to any norm-bounded subset of functions, it looks like an open set from the compact-open topology.
Where were we? Ah right, taking one of them, some arbitrary $U$, and generating a new strict-open neighborhood $U'$ where, for every $f\not\in U$, there's a strict-open neighborhood of $f$ that doesn't intersect $U'$.
So, pick an arbitrary $U$, alternately writeable as
$$U=\{f|\forall n:f(K_n)\subseteq(-a_n,a_n)\}$$
For some sequence of compact sets and numbers. Now, we can pick a $U'$ from the same local basis of 0 as follows.
$$U':=\{f|\forall n:f(K_n)\subseteq\left(-\frac{a_n}{2},\frac{a_n}{2}\right)\}$$
And, given some $f\not\in U$, here's how we generate its associated open neighborhood $U_f$. Given $f$, there must be some $n_f$ where $f(K_{n_f})\not\subseteq(-a_{n_f},a_{n_f})$. Let $x_f$ be some point from $K_{n_f}$ that lands outside that open. Then, let $U_f$ be defined as
$$\{g|g(x_f)\in\left(f(x_f)-\frac{a_{n_f}}{4},f(x_f)+\frac{a_{n_f}}{4}\right)\}$$
Alright, let's get going. Obviously, $0\in U'\subseteq U$. $U'$ and $U$ were both picked from the local basis of open neighborhoods of 0, so they're strict-open. All the $U_f$ are open in the compact-open topology, which is coarser than the strict topology so they're strict-open. Obviously, for any $f$, it's in $U_f$. That just leaves showing that if $f\not\in U$, that $U_f\cap U'=\emptyset$.
Let's say that there was a point in both sets, some function $g$. Then, $g(x_f)\in\left(f(x_f)-\frac{a_{n_f}}{4},f(x_f)+\frac{a_{n_f}}{4}\right)$ (since it's in $U_f$). And also, $x_f$ was picked to be a point where $f(x_f)\not\in(-a_{n_f},a_{n_f})$. If you work it out, $f(x_f)$ went either high or low, and in either case, $g(x_f)$ is distant from 0. In particular, we have $g(x_f)\not\in\left(-\frac{3a_{n_f}}{4},\frac{3a_{n_f}}{4}\right)$. However, we have
$g(x_f)\in\left(-\frac{a_{n_f}}{2},\frac{a_{n_f}}{2}\right)$ since $g\in U'$. Contradiction.
So, no point $g$ can be in both sets, $U_f$ and $U'$, they're disjoint. Since $f$ was arbitrary not in $U$, we have that every $f\not\in U$ has an open neighborhood $U_f$ that's disjoint from $U'$. And this argument goes through regardless of which $U$ we picked from the base, and we finally hit our proof target and everything's done.
