Actually, most of the paper seems a bit obvious from the computer science side. LLMs scale for really complex tasks, but they are neither correct nor complete. If combined with a tool that is correct (code verifiers, interactive theore provers), then we can get back a correct pipeline.
Many times the algorithm that you are implementing requires a precise data flow that is not reversible, so using traditional arithmetic (is/2) is better for catching errors.
On the other hand CLP(FD) is not new at all (it is very popular for constraint programming).
Why would it be better for error handling? If you'll be using unidirectional flow only, then the point is moot. But using clp is arguably better IMO, allowing type and range checks while allowing relational execution.
Bit different though! In your example, the video is made from manually syncing with the song bpm, as the beep is at a constant rate. It's basically just a hand-made visualization of (every other) kick drum.
While the submission has the notes not at a basic 1/4 tempo, and is automatically "animated" based on the constrained optimization. Also leads to a much more interesting visualization :)
Note that "CheerpX enables you to run existing 32-bit x86 native binaries".
For some reason support for wasm64 (in browsers) has been stagnated for years, which is a pity.
They should compare with other multithreading and GPU approaches for SAT/SMT solving (like https://www.win.tue.nl/~awijs/articles/parafrost_gpu.pdf from Armin Biere, or other works from Mate Soos). There has been a lot of research in this direction.
