I love posts/papers that review this history and I implore more people working in this field to share their perspectives and contributions to this amazing and very diverse practice. Future generations need to understand how ambitious & rich these last 50 years have been. Please share your stories!

For this year's #fsharp #FsAdvent, I'm announcing a preview of a .NET testing library I'm calling DenseCheck. DenseCheck is a systematic alternative to QuickCheck/FsCheck's random tester. Like FsCheck, DenseCheck automatically generates values from types! github.com/sgoguen/Dens...

Let the party begin! medium.com/@lanayx/the-... #fsharp #FsAdvent #oxpecker

F# Weekly #47, 2025 - F# 10 & last #FsAdvent slots #fsharp sergeytihon.com/2025/11/22/f...

This week we are chatting with Tomáš Grošup about #fsharp 10! amplifyingfsharp.io/sessions/202...

Attacks on trans women are attacks on women. I'm not sure why we don't see this. It will affect us on all levels of society. I will not have my womanhood policed, nor will I have others policed. Why do we not see this? Why do I even have to post that cis women are affected for cis women to care?

I'm still looking for 10 more #fsharp lovers to fill out the #FsAdvent schedule. 🙏

Hey #fsharp, what we do with #FsAdvent this year? sergeytihon.com/fsadvent/ Do we have 24 F#ers ready to participate?

I really enjoyed this year’s miniKanren ICFP presentations. While Gallois’s reversible Lustre-to-C compiler stole the show, I savored the modest talks just as much. www.youtube.com/live/OY9LVFV...

Has anyone watched this video that explains how cooperation games (Prisoner’s Dilemma) incentivize different strategies based on the shape/connectivity of the graph? What game(s) do players play on social media? What are the *real* +/- rewards/penalties? Can we abstract them? youtu.be/CYlon2tvywA

We really loved this series of tutorials on #metaprogramming in #LeanLang by Heather Macbeth. It's a great intro to a complex topic for novice users of #LeanProver! Pt 1: youtube.com/watch?v=cKvg... Pt 2: youtube.com/watch?v=5er4... Pt 3: youtube.com/watch?v=TJ8T...

If we were to model social media as a game -- algebraically, categorically or otherwise -- how can small groups of people play the game in a way that's contrary to the behavior the social media companies designed to incentivize? How many different ways can one play it "wrong"? Is there a cogame?

How should we proactively think & behave in an influencer fueled economy that incentivizes narcissistic confidence and disincentivizes humility & discernment?

One of the best things we can do with social media, at this time, is to make plans to spend time talking with a small group of people.

#MULCIA: Postdoc position to formalize machine learning algorithms in Lean. tinyurl.com/29sqjjx2 #PostDoc #AI #LeanProver

Glad to announce the miniKanren Workshop submission deadline has been extended 1 week, to July 17th anywhere on earth. conf.researchr.org/home/icfp-sp.... Looking forward to your submissions!

May 25-27, 2025, I hosted an event, the "Minnowbrook Logic Programming Seminar," in Blue Mountain Lake, NY. I recorded 11 talks on Datalog-related interests, totaling over 9+ hours of video, which I have just now published on YouTube youtu.be/3ec9VfMUVa8

This is a good talk explaining why Lean is more than a good proof assistant and what language folk can learn from the macro system and tooling.

I’m cool with studios green lighting Marvel movies without scripts, but I insist on Werner Herzog sitting the director’s chair. Herzog’s Batman would be amazing. variety.com/2025/film/ne...

Don't blame "the algorithm". Blame the people who dishonestly call it an "algorithm" for serving you slop. But above all, don't blame yourself for being bad at computer when it's computer that's bad at you.

If anyone has any slow or brittle Dafny/Boogie/Viper proofs, consider hiring me *hint* *hint* *nudge* *nudge* *wink* *wink* (I would normally be asking in person while presenting this work at CAV but again... I can't leave the country right now.)

The Choose-Your-Own-Adventure Calculus is a small formalism that captures an interaction pattern where you repeatedly choose from the available options. Examples include type providers, structure editors, theorem provers & more! Draft paper based on my earlier blog post: tomasp.net/academic/dra...

Has anyone on Bluesky been talking about how the entire climate team on NOAA was fired and the climate.gov website might be archived or repurposed?

Working on something that's getting me excited 🥰 For Fable 5 Python target we're rebuilding Fable Library in Rust to get proper .NET semantics when transpiling F# to Python. As a Python dev who fell hard for F#'s type system, this scratches an itch 🐍🦔🦀✨ #fsharp #python #fable #rust #pyo3

I'll be talking about my "Tiny programming systems" course & research at the #MoreVMs workshop in about 10 minutes. Join the @programming-conf.bsky.social live stream at: 2025.programming-conference.org ...and stay tuned for many great talks on Wednesday and Thursday!

Let G be a magma (i.e a set equipped with a multiplication and no further axioms). Can you prove that if ∀ x y z, x = x(y((zx)y)) then ∀ x y z, x = x(y(z(xz)))? You can use a theorem prover, a language model, a SAT or SMT solver or even pencil and paper. Terry Tao is collecting proofs of this! 1/2

We have an SDE II position on my team. No external link, but if I know you, you can send me your resume.

New blog post: How to (actually) prove it #Lean4 #LeanProver #Lean #ProgrammingLanguages kirancodes.me/posts/log-ho...

looks like the people at the Clay Institute are working over the weekend 😢

The Loan Programs Office (LPO) is one of the most quietly effective tools the federal government has. It is the center of our industrial policy providing loans that banks won't give for energy innovation. It funds real projects. Battery factories. Nuclear reactors. Geothermal energy. Car factories.

If you live in these rings, it may be worth going outside tonight and taking a few long-exposure photos of the Northern sky with your phone.

In case your wondering WHAT databases are being discontinued in NOAA. Um there’s ALOT.

Is Trump preparing to invoke the Insurrection Act? Signs are pointing that way www.sfchronicle.com/opinion/open...

The thing is, people who have double standards usually have double standards about having double standards. I can criticize *you* for being a hypocrite, but I'm quite comfortable with my *own* hypocrisy.

My "artistic" interpretation of '80s program synthesis using "Göddel" numbering. Keep turning that dial until you find the program that transforms your input into the given output!

I usually abhor most incarnations of drag/drop programming, but this educational proof construction tool is actually fun. Dragging connectors reveals the shapes. Proofs can be constructed forward and backwards. Selecting multiple blocks (w shift key) enables you to construct your own theorem/blocks

Looking to host a conference in North America? There are plenty of places 🇨🇦 that will make your attendees feel welcome!

[New Blog Post] Knuth Bendix Solver on Z3 AST #logic www.philipzucker.com/knuth_bendix...

Revisiting an early critique of formal verification. ~ Lawrence Paulson. lawrencecpaulson.github.io/2025/03/14/r... #ITP #Math #FormalVerification

Abject terror. The wealthiest and most powerful among us are in a state of abject terror.

One-by-one this administration will single out, harass, defund, attack, threaten, audit, and sue institutions, corporations and organizations that do not toe the authoritarian line unless we ALL stand up and say NO.

Transactions in Category Theory 2025 jademaster.xyz/TACT25.html It's going to be a thing.

Man, NSF fired tons of PMs, including some I know and really like, it seems. For example, tons of security folks and networking folks now gone. Seems particularly insane given the need to compete in security and networking versus (say) China.

Came across a toy/tutorial #fsharp project where you build a small verified language in F#. This slick tiny transpiler (maybe 800 LOC total) targets the Boogie language, which is then feed into Boogie's verifier, thus verifying your program. github.com/boogie-org/f...

run a quasi #fsharp quasi #ocaml lang on #arduino micro controllers ? yes - www.juniper-lang.org

Where are all the rewrite rules? If you know of where some are, please let me know. www.philipzucker.com/rewrite_rules/

It's LAB GIRLGATE! No seriously lmk if you want a copy of my new one ADVENTURES OF MARY JANE. I need honest reviews on that one because they are fixing to ban the hell out of it 'cuz it dares to feature a gender-ambiguous character 😱. The @wsj.com has already pilloried it twice.

I have this ridiculous obsession with bijective Gödel numbering systems that I can’t shake off. Plainly put, a bijective Gödel numbering system lets you encode programs as integers in a way where each integer encodes/decodes to a unique program. So, what does this have to do with this code? 🤷‍♂️ 1/n