Where can I find the miniscript policy language specification? I would like to understand how miniscript works by coding it myself. As I started studying it, I realized that miniscript is more or less a 1-for-1 abstraction of a subset of Script and that the policy language implementation would shed more light on how miniscript is beneficial.

I haven't found any specification on how the policy language to miniscript language compilation works, just what I've found here: http://bitcoin.sipa.be/miniscript/

Besides the raw code, is there a description of how the policy language compiles to miniscript?
There is no specification, or really documentation, for Miniscript other than sipa's website. There is no "correct" or singular way to compile a miniscript policy into miniscript. The two existing implementations actually go about compiling in different ways, although both arrive at the same result (occasionally they differ, but the two results are semantically the same but are equally optimal). The only thing to be concerned about are whether the miniscript is optimal, and whether it is semantically the same as the policy.

Checking whether it is semantically the same is trivial. A miniscript can be "lifted" into policy by dropping tags and types so it is easy to check that a compiled miniscript is semantically the same as the policy.

Checking whether a given miniscript is optimal generally boils down to its size and expected satisfaction size. Smaller is better, so a miniscript whose end scriptWitness size is the smallest is considered to be optimal. When considering policies that include probabilities, the expected value should be taken into account.

As for compiling from policy into miniscript itself, there are different strategies. One strategy (which I believe is actually done in one of the libraries) is to construct every possible miniscript for a given policy and just select the optimal one.