A language for scalable data analysis, ACL2 for Trustworthy Vibe Coding, lghtnng

Hello, hacker ladies and gentlemen!
We're meeting in San Francisco this time. Hima Tammineedi of Forge is hosting us at 6pm on Tuesday, January 13th. (Thank you!) We'll have two long-form talks, perhaps some five-minute lightning talks, and socializing afterwards.
Forge is at 2323 Hyde St. Please note that parking is limited, so Hima recommends that we use Uber or some other transportation that doesn't require parking. Also, note that the offices are on top of a hill. Forge will provide food (tacos), so please RSVP so we can have an accurate count.
Our first talk will be A language for scalable data analysis, by Mike Dixon.

> Proposing a new programming language is “a classic blunder, … (second only to) starting a land war in Asia”. But.
> Exploratory analysis of large datasets is an increasingly common need that is poorly served by existing tools. I think we can do much better than the current state-of-the-art, and that doing so will involve (among other things) a new language.
> Retrospect is an open-source project (based on work originally done at Google) pursuing these ideas. I’ll describe the progress so far, a language with
>
> * strictly immutable values
> * map/reduce as a core operation
> * design to support efficient parallel and distributed execution
> * performance closer to C than to Python
>
> … and talk about what comes next.
> Mike’s career has hopscotched from working on Interlisp and 3-Lisp at PARC, to a web-conferencing startup, to helping Google News grow out of its pile-of-perl-scripts origin, to building Earth Engine (probably the largest lambda-reduction service on the internet). He retired a few months ago and is still figuring out what that means.

Next will be ACL2 (A Computational Logic for Applicative Common Lisp) for Trustworthy Vibe Coding, by Jim White.

> Generative AI enables rapid "vibe coding," but often lacks the rigor required for high-assurance software. This talk explores bridging the gap between stochastic LLM capabilities and formal verification using ACL2 (https://github.com/acl2/acl2), an industrial-strength automated reasoning system for Common Lisp. I will demonstrate making agents with assurances as a step towards "Theorem Driven Development".
> Technical details will focus on the practical application of SMTLink to harness the Z3 SMT solver within the ACL2 environment. We will examine how this enables the implementation of verified code, including LLM-powered agents, and discuss work-in-progress aimed at transpiling these verified Lisp models into executable Python and JavaScript.
> Jim White’s journey into logic and language began in the S-100 era, loading FORTH from Tarbell cassette tapes and writing binary on an IMSAI 8080 before landing his first high school contracting gig on a PDP-11/03. At UC Irvine, inspired by Gödel, Escher, Bach, he studied under Jim Meehan (UCI LISP), where he built a visual LISP structure editor and first conceived the Program Understanding Program (PUP). After a diverse engineering career - ranging from implementing LISP in FORTH for the NS32000 to leading Google Assistant phone line projects. Jim earned an M.S. in Computational Linguistics to apply NLP methods to code as a corpus. Currently the founder of Wiki3.ai, he is working to realize the long-term vision of PUP by combining local-first AI with formal methods, ensuring that AI-generated code is verifiable and trustworthy.

Please join us in person. (I'll do my best to record the talks, but I won't live-stream them.) After the talks, we'll mingle and have snacks. Good things come from meeting in person.
Thank you, Hima and Forge!
#balisp #san-francisco