Additional shout out to the Recurse Center (https://www.recurse.com/) which was instrumental in giving me the space and environment to start working on Dusa. I did a partially-remote, partially-in-person batch at Recurse in late 2023.
As someone whose day job involves a lot of graph analysis and logic programming[0], I'm always excited to see new applied research in this area. More energy is needed here.
Logic systems will be a key part of solving problems of hybrid data analysis (e.g. involving both social graphs, embedding spaces, and traditional relational data) - Cozo[1] sticks out as a great example.
Is there an implicit algorithm for how this language is evaluated? It seems hard to use without having an understanding of the likely performance of your code.
There is an implicit algorithm, and I'm so happy about this question. The inability to reason about likely performance of one's code is, to me, one of the things that bothers me most about Answer Set Programming, the programming paradigm that's probably the most like Finite-Choice Logic Programming.
The Dusa implementation has a couple of ways to reason at a high level about the performance of programs. The academic paper that febin linked to elsethread spends a fair amount of time talking about this, and if you really want to dig in, I recommend searching the paper for the phrases "deduce, then choose" and "cost semantics".
There's work to do in helping non-academics who just want to use Dusa reason about program performance, so I appreciate your comment as encouragement to prioritize that work when I have the chance.
...and if you're in the vanishingly small overlap of folks reading this comment and people interesting in attending an academic talk in Denver next Wednesday, the official conference page for the paper is https://popl25.sigplan.org/details/POPL-2025-popl-research-p...
I want to say that the cultural changes inside of the ACM to make historical research open access and to have excellent live streams of the conferences is just so damn wholesome and wonderful. Thank you ACM and the people inside the ACM that made this happen.
And in case someone from the ACM is reading this, the live streams are very useful for physical attendees. I was attending Splash! and there were a ton of talks where I would have needed to change rooms, wanted lots of desk space for notes and research. It was somewhat ironic attending half a day from a vacation rental. :)
Genuinely asking: what are the advantages of this approach with other approaches like Prolog? How is the interplay between current state-of-the-art, and finite-choice logic programming over what was previously known about logic programming?
Unfortunately, starting from a perspective that logic programming is mostly Prolog is a pretty bad way of getting to understand what Dusa is about. There's nothing wrong with that starting point, it's just... kind of like trying to understand Kotlin because you learned Smalltalk and know that both are object-oriented.
The linked page suggests one intro if you have experience with Datalog, another intro if you have experience with Answer Set Programming (ASP), and a third for everyone else. That's because Datalog and ASP are the two logic programming things that are most like finite-choice logic programming. Finite-choice logic programming gives a completely new way of understanding what answer set programs mean. The Dusa implementation is able to solve some problems vastly more efficiently than state-of-the-art ASP solvers, and is able to easily solve other problems that mainstream ASP solvers are simply unable to handle because of something called the "grounding bottleneck." Right now it's not a strict win by any means: there are many problems that Dusa chokes on that state-of-the-art ASP solvers can easily handle, but we know how to solve at least some of those problems for implementations of finite-choice logic programming.
All implementations of Answer Set Programming I am aware of are actually Turing complete, as are many practical implementations of the Datalog idea, and so is Dusa — this is a common misconception!
From the paper: "often people take “Datalog” to specifically refer to “function-
free” logic programs where term constants have no arguments, a condition sufficient to ensure that every program has a finite model. We follow many theoretical developments and practical implementations of datalog in ignoring the function-free requirement." If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.
>> If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.
What is the reverse here? Sorry it's late and I can't calculate it.
Btw, what I know about ASP is that it is incomplete (in the sense of soundness and completeness). Turing completeness is a separate question.
If every program has a finite model, the language cannot be Turing complete.
If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.
(For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
>> If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.
Thanks, yes, that makes sense. But I'm not convinced of arguments "in practice". In practice, why do we care about Turing completeness? It's not like anyone sells infinite tape. But "in practice" we end up having no idea what are the limits of this or that system, so some principled reasoning is sometimes useful... practically useful.
>> (For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
Relative to proofs: a proof procedure is complete if, when there exists a proof of some formal statement, the procedure can always derive that proof. Consider Resolution; say A |= B; then there exists a Resolution-refutation of A ∧ ¬B (i.e. the derivation of the empty clause A ∪ ¬B ⊢ □) so Resolution is refutation-complete. As far as I understand it this is not the same as Turing completeness, which is about a system being able to compute every program a Universal Turing Machine can compute. E.g. the first order predicate calculus is Turing complete and its restriction to Horn clauses is also Turing complete, but that doesn't necessarily imply the existence of a complete proof procedure for Horn clauses- that has to be shown separately.
Or at least that's how I think about it. I might be dead wrong there so please correct me if you have a better understanding of this than me.
There are many useful things that are not turing complete and still considered programming.
Regular Excel formulas are always terminating and therefore not computationally complete.
SQL without recursive CTEs is always terminating and therefore not computationally complete.
Simply typed lambda calculus is always terminating and therefore not computationally complete.
It's not the same, but restriction to terminating subsets gives very nice guarantees for a lot of program properties that would otherwise be undecidable.
I don't have any problems with calling it programming even if it's not Turing complete. But I think it's nice to clarify, so I can understand where it is in the expressivity-landscape.
Maybe it's obvious for the intended audience, given the mention of Datalog? But I suspect a lot of compsci people know of Prolog, and know about SAT(and similar) solvers, but don't really know how e.g Datalog places.
> Answer set programming is a way of writing Datalog-like programs to compute acceptable models (answer sets) that meet certain constraints. Whereas traditional datalog aims to compute just one solution, answer set programming introduces choices that let multiple possible solutions diverge.
Fascinating! I could see useful applications in litigation (e.g., narrowing potential claims; developing the theory of the case; finding impeaching lines of questioning).
Indeed — answer set programming has been used for this purpose, see https://arxiv.org/pdf/2212.06719 (which was co-authored by Chris Martens, the co-designer of Dusa and the primary author of the Finite-Choice Logic Programming paper).
> Note that this if-then statement is written backwards from how it’s written in English: the “then” part, the conclusion is written first, followed by the :- symbol. After the :- symbol come the premises
Why not write it like it’s written in English? It could be one less thing to learn for people trying to adopt the language.
The two answers by jonjojojo and khaledh are great, because they are both the correct answers.
From a principled point of view, the rule "a :- b, c" helps define what "a" means, and it seems, in practice, most helpful to be able to quickly visually identify the rules that define a certain relation. The list of premises tends to be of secondary importance (in addition to often being longer and more complicated).
From a practical point of view, we wrote Dusa as people familiar with existing Datalog and Answer Set Programming languages, which use the backwards ordering and ":-" notation, and some of the core target audience we hope to get interested in this project is people familiar with those languages, so we made some syntax choices to make things familiar to a specific target audience. (Same reason Java uses C-like syntax.)
The :- is supposed to sort of look like a left facing arrow for an implication.
I think this notation started with prolog, so that is my guess why they chose to make it like this.
I think the reason is that the right hand side can be a long and complex set of premises. It is supposed to be read as: The lhs is true iff everything on the rhs is true.
You can also think the same way about functions in typical languages: we don't write the body of the function first and then assign it to an identifier.
With those two statements, `f(a)` is true, but it does not mean that `g(a)` and `h(a)` are also true. Instead, it means that we happen to know some fact, `f(a)`, and some rule for cases beyond that fact. If it also happened that `g(a)` and `h(a)` are true then we'd have two ways of arriving at the fact of `f(a)` being true.
It's a reverse of the implication arrow and is meant to be read that way:
f(X) :- g(X), h(X).
Is read as "f(X) if g(X) and h(X)", versus "if g(X) and h(X) then f(X)".
not only do I think that choice is a really important tool for writing pragmatic logic programs, this is a key piece to a really interesting goal - unifying logical and procedural programming (see verse)
Have to admit as a “regular”
developer using general purpose languages such as Java, C, Ruby, Perl, etc., most of this goes over my head, but at the same time I find the mix of Prolog and VB syntax fascinating and confusing.
What do you consider a real life task, if Graph reachability, Graph coloring nor finding Connected components count? They all have many straightforward applications.
My mind is blown, a new language where I can see new reach. Back in the day, APL was good at multidimensional arrays, and from there could outstrip Fortran shops at anything. A surprising swath of discrete reality can be viewed as a graph, or graphs of graphs. For me, computational group theory, combinatorial enumeration, canonical forms... All topics Claude 3.5 Sonnet happens to be exceptional at.
Even a month ago, I'd have asked "Where's the parallelism?" looking at any new language. AI has upended my world. My subscriptions are getting out of hand, they're starting to look like some peoples' sports channel cable bills. I'll be experimenting with the right specification prompt to get AI to write correct programs in three languages side by side, in either Cursor or Windsurf. Then ask it to write a better prompt, and go test that in the other editor. I'm not sleeping much, it's like buying my first Mac.
One constant debate I have with Claude is how much the choice of language affects AI reasoning ability. There's training corpus, but AI is even more appreciative of high level reasoning constructs than we are. AI doesn't need our idioms; when it taught itself the game Go it came up with its own.
So human documentation is nice, but who programs that way anymore? Where's the specification prompt that suffices for Claude to code whatever we want in Dusa?
Also potentially interesting to this crowd are the underlying editor, which I split out from the online Dusa editor and called "sketchzone" (https://github.com/robsimmons/sketchzone). Some of my motivations and hopes for sketchzone are blogged here: https://typesafety.net/rob/blog/endless-sketchzone
Also, I more-or-less did Advent of Code 2024 in Dusa: journal entries and links to solutions are at https://typesafety.net/rob/blog/advent-of-dusa-2024
Zig was also apparently partly developed whilst Andrew Kelley was there. Fun place.
Logic systems will be a key part of solving problems of hybrid data analysis (e.g. involving both social graphs, embedding spaces, and traditional relational data) - Cozo[1] sticks out as a great example.
[0] https://codeql.github.com/docs/ql-language-reference/about-t...
[1] https://www.cozodb.org/
The Dusa implementation has a couple of ways to reason at a high level about the performance of programs. The academic paper that febin linked to elsethread spends a fair amount of time talking about this, and if you really want to dig in, I recommend searching the paper for the phrases "deduce, then choose" and "cost semantics".
There's work to do in helping non-academics who just want to use Dusa reason about program performance, so I appreciate your comment as encouragement to prioritize that work when I have the chance.
(The ArXiV preprint has the exact same content)
https://popl25.sigplan.org/attending/live-streams
I want to say that the cultural changes inside of the ACM to make historical research open access and to have excellent live streams of the conferences is just so damn wholesome and wonderful. Thank you ACM and the people inside the ACM that made this happen.
And in case someone from the ACM is reading this, the live streams are very useful for physical attendees. I was attending Splash! and there were a ton of talks where I would have needed to change rooms, wanted lots of desk space for notes and research. It was somewhat ironic attending half a day from a vacation rental. :)
The linked page suggests one intro if you have experience with Datalog, another intro if you have experience with Answer Set Programming (ASP), and a third for everyone else. That's because Datalog and ASP are the two logic programming things that are most like finite-choice logic programming. Finite-choice logic programming gives a completely new way of understanding what answer set programs mean. The Dusa implementation is able to solve some problems vastly more efficiently than state-of-the-art ASP solvers, and is able to easily solve other problems that mainstream ASP solvers are simply unable to handle because of something called the "grounding bottleneck." Right now it's not a strict win by any means: there are many problems that Dusa chokes on that state-of-the-art ASP solvers can easily handle, but we know how to solve at least some of those problems for implementations of finite-choice logic programming.
From the paper: "often people take “Datalog” to specifically refer to “function- free” logic programs where term constants have no arguments, a condition sufficient to ensure that every program has a finite model. We follow many theoretical developments and practical implementations of datalog in ignoring the function-free requirement." If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.
What is the reverse here? Sorry it's late and I can't calculate it.
Btw, what I know about ASP is that it is incomplete (in the sense of soundness and completeness). Turing completeness is a separate question.
If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.
(For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
Thanks, yes, that makes sense. But I'm not convinced of arguments "in practice". In practice, why do we care about Turing completeness? It's not like anyone sells infinite tape. But "in practice" we end up having no idea what are the limits of this or that system, so some principled reasoning is sometimes useful... practically useful.
>> (For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
Relative to proofs: a proof procedure is complete if, when there exists a proof of some formal statement, the procedure can always derive that proof. Consider Resolution; say A |= B; then there exists a Resolution-refutation of A ∧ ¬B (i.e. the derivation of the empty clause A ∪ ¬B ⊢ □) so Resolution is refutation-complete. As far as I understand it this is not the same as Turing completeness, which is about a system being able to compute every program a Universal Turing Machine can compute. E.g. the first order predicate calculus is Turing complete and its restriction to Horn clauses is also Turing complete, but that doesn't necessarily imply the existence of a complete proof procedure for Horn clauses- that has to be shown separately.
Or at least that's how I think about it. I might be dead wrong there so please correct me if you have a better understanding of this than me.
Regular Excel formulas are always terminating and therefore not computationally complete.
SQL without recursive CTEs is always terminating and therefore not computationally complete.
Simply typed lambda calculus is always terminating and therefore not computationally complete.
It's not the same, but restriction to terminating subsets gives very nice guarantees for a lot of program properties that would otherwise be undecidable.
Maybe it's obvious for the intended audience, given the mention of Datalog? But I suspect a lot of compsci people know of Prolog, and know about SAT(and similar) solvers, but don't really know how e.g Datalog places.
> Answer set programming is a way of writing Datalog-like programs to compute acceptable models (answer sets) that meet certain constraints. Whereas traditional datalog aims to compute just one solution, answer set programming introduces choices that let multiple possible solutions diverge.
Fascinating! I could see useful applications in litigation (e.g., narrowing potential claims; developing the theory of the case; finding impeaching lines of questioning).
Why not write it like it’s written in English? It could be one less thing to learn for people trying to adopt the language.
https://dusa.rocks/docs/introductions/graph/
From a principled point of view, the rule "a :- b, c" helps define what "a" means, and it seems, in practice, most helpful to be able to quickly visually identify the rules that define a certain relation. The list of premises tends to be of secondary importance (in addition to often being longer and more complicated).
From a practical point of view, we wrote Dusa as people familiar with existing Datalog and Answer Set Programming languages, which use the backwards ordering and ":-" notation, and some of the core target audience we hope to get interested in this project is people familiar with those languages, so we made some syntax choices to make things familiar to a specific target audience. (Same reason Java uses C-like syntax.)
You can also think the same way about functions in typical languages: we don't write the body of the function first and then assign it to an identifier.
It's a reverse of the implication arrow and is meant to be read that way:
Is read as "f(X) if g(X) and h(X)", versus "if g(X) and h(X) then f(X)".if (want: edge Y X) { search for: edge X Y }
This is searching in reverse compared to a different if statement:
if (have: edge X Y) { assert: edge Y X }
No, what I want is a code example, front and center.
Even a month ago, I'd have asked "Where's the parallelism?" looking at any new language. AI has upended my world. My subscriptions are getting out of hand, they're starting to look like some peoples' sports channel cable bills. I'll be experimenting with the right specification prompt to get AI to write correct programs in three languages side by side, in either Cursor or Windsurf. Then ask it to write a better prompt, and go test that in the other editor. I'm not sleeping much, it's like buying my first Mac.
One constant debate I have with Claude is how much the choice of language affects AI reasoning ability. There's training corpus, but AI is even more appreciative of high level reasoning constructs than we are. AI doesn't need our idioms; when it taught itself the game Go it came up with its own.
So human documentation is nice, but who programs that way anymore? Where's the specification prompt that suffices for Claude to code whatever we want in Dusa?