Announcing CSLib

Stream: CSLib

[Clark Barrett]

I'm happy to announce the new CSLib channel. This channel will host discussion regarding the emerging CSLib effort, an initiative to formalize undergraduate Computer Science in Lean. An introduction to the effort will be held via Google Meet on at 2025-07-02T08:00:00-07:00 . All are welcome to join. The meeting info is below.

[Shreyas Srinivas]

Are you familiar with existing efforts and previous discussions on this topic?

[Clark Barrett]

Video call link: https://meet.google.com/hut-zidv-mcu

[Shreyas Srinivas]

I think there are quite a few threads and now active repositories on this topic. We should probably link them in here as references.

[Clark Barrett]

Yes, we are interested in unifying these efforts. Our effort is supported by Amazon, DeepMind and LeanFRO. But it is just getting started, so we need lots of volunteers. That's part of what tomorrow's meeting is about.

[Shreyas Srinivas]

Okay. In that case I propose that we at least discuss one basic question: Whether it even makes sense to have a unified CS library. There is such a wide gulf between different areas of CS that needs bridging.

I am doing my PhD working with algorithms theorists. Even within algorithms theory, the notion of a sequential algorithm is not very well defined, especially once we start talking about models. I have been writing my thoughts (and privately some incomplete code on some algol like language) based on the notion that all algorithms are queries + combinators in disguise and at some level that is what the average STOC/FOCS/SODA theorist actually works with and counts for complexity purposes. So we need a combinator inductive type parametrised by a query type with mechanisms for WF recursion to prove termination. It unifies a lot of models of computation, including impractical ones using real numbers.

In the European TCS community there is a clear line between so called Track A and Track B theorists as seen at conferences like ICALP and ESA. Likewise, Distributed algorithms folks and distributed systems folks mostly work on very different models with some overlap. There is an ongoing project here on this server, just to clearly define some of the distributed algorithms models and relations between them

[Clark Barrett]

We have a well-defined subset we are going to start with. And we are building a DSL for describing computation. Please come to the meeting if you'd like to know more!

[Kim Morrison]

I'm excited to see this, and will stay up late for the meeting. :-)

I hope we can design it from the ground up so that grind deals with as much boring stuff as possible! I'll be happy to help on that front.

At the FRO we're also thinking about a refresh of our cross-repository testing infrastructure, and we'd very much like to include CSLib in whatever we do next here, to make sure that changes in Lean have only positive effects on the project!

I'm really looking forward to seeing the roadmap and scope for CSLib.

[David J. Webb]

Having just taught undergrad algorithms, I'm looking forward to seeing where this goes!

Can't make the meeting (5 am my time), but I will look at the minutes/summary/roadmap

[Shreyas Srinivas]

There will be many people who have similar time zone issues or will be otherwise engaged. Could we have a recording of the meeting posted here?

[Swarat Chaudhuri]

We will record the meeting, and there will be another meeting next Wednesday at the same time.

[Eric Taucher]

CSLib Discussion: July 2, 2025

Please put your questions about the CSLib effort in this document. We will try to respond to all questions, some verbally during the meeting and some in written form offline.

https://docs.google.com/document/d/1d0mwj3IMC4ucYjHaD5glpEIQhJ4YhnWsl8nyQL_jYHo/edit?pli=1&tab=t.0#heading=h.elxu16sem8xl

[Eric Taucher]

Links to slides

https://docs.google.com/presentation/d/1aJFM3EaI4LcppHR_2YFQHiBjUfMMhMKxCeM3BfINi48/edit?slide=id.g34fce84c8b2_0_3#slide=id.g34fce84c8b2_0_3

[Shreyas Srinivas]

Is there published information about the application procedure for PIs to apply for the two funded positions? EDIT: I am asking so that I can forward it to people in the algorithms theory research community who might be interested.

[Clark Barrett]

Shreyas Srinivas said:

Is there published information about the application procedure for PIs to apply for the two funded position?

Making this information available is a top priority. Stay tuned.

[GasStationManager]

I just heard about this, so unfortunately missed the google meeting. This is very cool!

Looking forward to learning more about this as more information become available. One quick comment about Boole (sorry if this is covered in the meeting): If we are to go through the trouble of adopting a DSL, I really hope that it doesn't stop at complexity/resource usage, and can in principle be extended to reason about all real-world effects of programs, such as input/output and networking.

If one were to adopt the worldview of Guaranteed Safe AI, we need to build world models as part of safe AI systems. I see complexity/resource usage as one part of a larger world model. Boole has the potential of becoming such a world model for computer programs, if it can be made general enough.

[Bas Spitters]

Boole is a language in the Amazon MIDI family

Is there more information available about Boole or the MIDI family? Google was not helpful...

[Ayhon]

As I understood, Amazon MIDI is currently internal, and to be released by the end of the month, while Boole is yet-to-be-defined

[Ayhon]

But wait for someone else to confirm before concluding Im right

[Clark Barrett]

Yes - that is correct. So unfortunately, you'll have to wait for the Amazon release to get your hands on MIDI and Boole.

[Bas Spitters]

Thanks @Clark Barrett is there an ETA for that?

[Bas Spitters]

I see it's in the slides:

Early August: Definition of initial version of Boole

[Alex Meiburg]

A good chunk of "complexity" is only reasonably describable in terms of I/O and side-effect laden behavior. Streaming algorithms, query complexity, and communication complexity, for instance, all require some kind of "request more input". (Randomized algorithms can be done without this, but I think are most natural if you can "request a random bit".)

I think this makes a good case that, even if this was entirely about "undergrad complexity theory", it would need to extend beyond just the "internal" metrics of time and space usage.

[Shreyas Srinivas]

My impression is that this project doesn’t care about such models, although these might very well appear in an upper undergrad course depending on the university. The notion of “undergrad curriculum” in CS is incredibly broad and diverse.

[Ayhon]

My impression was, rather than it doesn't care, that it's not their priority for now, but that they'd be interested in supporting this through dialects of Boole

[Shreyas Srinivas]

Nothing presented so far suggests support for user specified complexity models even in the sequential realm. If one needs dialects for every model then I am not optimistic about them being covered anytime soon.

[Shreyas Srinivas]

This is fine since there are entirely too many models to fit into one box. Meanwhile projects outside this library are bound to continue chugging along perfectly fine by themselves (including mine). So it is fine if this library doesn’t cover all models. A diversity of efforts is good for the community.

[Clark Barrett]

The second iteration of our CSLib discussion is happening shortly: 2025-07-09T08:00:00-07:00. This will be a repeat of last week's presentation for those who missed it. The link is: https://meet.google.com/xgn-efnm-czp?hs=224

[Paulo Matos]

Clark Barrett said:

The second iteration of our CSLib discussion is happening shortly: 2025-07-09T08:00:00-07:00. This will be a repeat of last week's presentation for those who missed it. The link is: https://meet.google.com/xgn-efnm-czp?hs=224

Are these meetings recorded by any chance?

[Pieter Cuijpers]

Is there a link to the recordings of these meetings?

[Alexandre Rademaker]

Hi Pieter,,as far as I know, no recordings.