!/0 is the cut. It prunes the search space. Useful to say "do not look at the other alternatives since I know they will fail" (when mutually exclusivity is hard) but also necessary to do negation in Prolog (when negated information cannot be easily or efficiently propagated).
is/2 is arithmetic evaluator. It runs only in one direction and it does not solve equations.
#>, #=, etc. are constraints, like (in)equalities over linear arithmetic. When constraints have the form of some known theory (like in SMT solvers), they can be solved (incrementally). That is called "constraint logic programming" (CLP). Modern Prolog systems are indeed CLP systems.
Prolog is older than CLP. CLP is older than SMT. Prolog+CLP systems are turing complete, can be used as programming languages. SMT is powerful but not a programming language.
Can "impure" features be avoided? Not in all cases. Think of them as 'unsafe' in Rust, but less dangerous.
Markus pushes for more purity in Prolog (using CLPFD), but sometimes some impurity (or imperative-like code with side-effects) is the best solution. Sometimes the pure solution is also the better. In other cases, it is not. Better compilers and static analyzers can reduce the friction between these worlds.
Take away: do pure code if you can afford it and it looks like a natural solution to your problem, use impure features later if you really need them.
I think in many real-life cases it's a mix - for example impure code that deals with the outside world to set up the data needed for the pure "core" of the app to run over.
usually you're more interested in better ergonomics: can you do X with less work?
it's like picking a programming language - depending on what you're attempting, some will be more helpful.
and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"
the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.
Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types.
Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.
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 :)
is/2 is arithmetic evaluator. It runs only in one direction and it does not solve equations.
#>, #=, etc. are constraints, like (in)equalities over linear arithmetic. When constraints have the form of some known theory (like in SMT solvers), they can be solved (incrementally). That is called "constraint logic programming" (CLP). Modern Prolog systems are indeed CLP systems.
Prolog is older than CLP. CLP is older than SMT. Prolog+CLP systems are turing complete, can be used as programming languages. SMT is powerful but not a programming language.
Can "impure" features be avoided? Not in all cases. Think of them as 'unsafe' in Rust, but less dangerous.
Markus pushes for more purity in Prolog (using CLPFD), but sometimes some impurity (or imperative-like code with side-effects) is the best solution. Sometimes the pure solution is also the better. In other cases, it is not. Better compilers and static analyzers can reduce the friction between these worlds.
Take away: do pure code if you can afford it and it looks like a natural solution to your problem, use impure features later if you really need them.