What I did today. High volume, low context. Sometimes nonsense. (Archive)
Dormant Last read · last published · next check
Read 8 days ago and current, but nothing has been published for 18 months.
I worked on another AI coding project, but this time, it was on a project and a language stack that I had no experience in (TypeScript and Vue), giving me some calibration on what it is like to work on an AI coding project on a preexisting (though not too large) codebase. Some overall thoughts: RAG was kind of hit or miss. It felt really good when Cursor was able to find the right spot to edit…
I played around with compiling/exporting some TTS models, specifically Kokoro and Zonos. Zonos I got to export successfully, see https://github.com/Zyphra/Zonos/pull/57. I did this in a series of public livestreams, which I also recorded and will eventually upload to YouTube. This produced some juicy guidance for the export team at Meta. It also made me realize that we really need to update our…
Well, I finished my scraper: I can feed it the page I want scraped, and it will go and download everything I want and put it into a bunch of files on my filesystem, one per entry. I have mixed feelings about the AI coding experience. Let’s try to tease them apart. The good: Not having to actually write code reduces cognitive load. I still have to design, fix bugs, do testing, iterate on UX,…
Yesterday was a rest day, I bought a new laptop and played around with deep research. I also had a lovely chat with some folks at Cursor, Sualeh kindly nudged me into using Composer, which is what I did a lot of today. What I did: I tried the puppeteer MCP to see if it can do direct scraping with just Cursor Agent. It sure seems like it’s doing something! But as best I can tell, the actual…
Read a bunch of papers, Discords, Reddits, OpenAI’s documentation, blog posts. I also tried redoing my scraper with uv and trying out a “write design doc and then make the LLM one shot it”, this resulted in a funny death spiral where my chromedriver was busted and the right fix was to just delete .wdm but the agent just kept trying all sorts of random crap that didn’t work.…
What I did: Figured out how to make Chrome not advertise itself as an automation Attempted and gave up to switch to Firefox as part of doing this Got the end-to-end POC going. Will need to consult with customer (aka my wife) more about requirements for what we need on top of it I listened to Sasha Rush’s Deepseek video: https://www.youtube.com/watch?v=0eMzc-WnBfQ Read a bit about how to use…
I’m reviving this blog to write some notes about LLM application explorations that I’m doing for fun during my parental leave. I’ve also been tweeting my journey but this will be a bit more digested. What I did: Installed Cursor (hooray 14 day trial) Read the Cursor docs Cursor works with Jupyter! Use Cmd-K to write lots of code in Playwright and Selenium that I’ve never…
Best way to hunt is to find some temporary accommodation near where you are looking, show up, and then just full-time apartment hunt for a few days, tagging listings as they appear in real time. Make sure you have CERTIFIED checks, not normal checks. They cost $2-10, and you’ll probably need at least two. Make sure your bank is local enough so you can pick up some quickly. You can get a…
In Dreyer’s “A Type System for Recursive Modules” (also known as the RMC paper), there is something very curious going on with the inference rules: in order to support recursive signatures and modules, RMC must do a pre-pass before doing the typechecking pass proper. This is actually quite common in recursive module systems (e.g., you see it again in MixML). In RMC, there are…
FP encourages equational reasoning! In Haskell, in practice: type class laws, RULES Reasoning by hand: tedious! Easy to gloss over details without mechanical support. (So not done in practice) HERMIT: interactive/scripted transformation on core IDEA: add lemmas to HERMIT. Equivalences beween core expressions; support conjunction, disjunction, implication, quantification Then redo KURE,…
Consistent use of units is a good idea! Typechecker? Goal: stop unit errors, and type inference, and make conversions (type classes). (Demo!) (beautiful type error.. But at the top, it just says it couldn’t match m/s with s) (exponentiation and derived units work in TH quasiquoter.) (convert has an unpleasant type) “Adam, when the demo doesn’t work, click here.” Type…
A talk for solving numeric constraints in Haskell programs Example: length-indexed vector reverse What are the generic things a Haskell compiler has to do? This results in a nice integration with SMT. The main point of a Haskell compiler is to get implications. GHC can do forward reasoning: you can assume facts that are implied by assumptions. Also, unsatisfiable assumptions are unreachable.…
This involves two things: checking exhaustiveness, and checking redundancy. Additionally in Haskell, we want to account for laziness; we also want to reason about exotic features like view patterns. Example: zip [] [] = [] zip (x:xs) (y:ys) = (x,y):zip xs ys Notice this is not exhaustive: input lengths are not necessarily the same length. So we get a warning saying they’re not exhaustive.…
Solve the subproblems independently! let x = "hi" in not x Claim: x is an error source; there is a change to this place which can make it well typed. So now you replace it with a hole: let x = "hi" in not ? and now it’s well typed. In general, there might be many, so the error source is a set. Now, also there are possibly multiple error sources, where fixing any one is OK. So for example,…
Built a language to express these contracts. American Option. At any time in the next 90 days, party X may decide to buy EUR 1000 from party Y for a fixed rate 1.1 of USD. Our contract language: we have transfers, composed conjunctively with a scaled version of the transfer (scaled). The option itself is a conditional which is bounded over a range, and checks if the condition is true. obs() checks…
GUI programs often have mutable state. How do we avoid it? FRP. Problems: space leak (forget the past), no I/O interface (change the future) Goal: get rid of space leaks with out fancy types and getting rid of higher-order programming Time -> a; (Time, a) Leak: snapshot :: Behavior a -> Event () -> Event a (need to keep all of the old behavior) More general: whenJust :: Behavior (Maybe a) -> Event…
Motivation: LVish. Need to provide data structures. We don’t know if your program has a big contended map, or a bunch of small contended map. So they have a few implementations of data structure variants, at the cost of complexity. Standard data structure: map in an IORef. Pure data in a box is useful because of constant time snapshots, and lock freedom: if you atomically access the IORef,…
About unification in Coq today. Write a Coq function which maps zero to zero. He tries to be clever and write (fun x => _) and Coq can fill in underscore with x. But then he tries to write _ and Coq says no unifier is found. Hmm, somehting is fishy. Another assignment: in_head : In a (a :: l) in_tail : In a l -> In a (b :: l) inR : In a r -> In a (append l r) Try to prove something…. and it…
On Georg Neis not being able to give the talk: “George Neis is starting at Google, while is old boss and his new boss are enjoying themselves at ICFP.” Georg Neis is actually the driving force for this project. Pilsner is the first compiler for a higher-order imperative (ML) language which has been compositionally verified. The starting point for this work is this field on compiler…
Thank you for the opportunity come and rant, unconstrained by science! (laughter) What I plan to do: show you some stuff I think is interesting, in the hope of luring you into FP and hardware design. I consulted some oracles (who work at the coal-face of hardware design); this is a mixture of things I like and they told me about. Let’s start about hardware description languages. How old are…