Post

They say PL people only produce languages that are good for implementing languages but that pathology seems laughably tame compared to LLM frameworks/orchestrators…

Amber 🌸

@shimmermathlabs.com

5 May

obviously need to combine the two languages for creating orchestrators, or orchestrators for creating languages, hmmm

Amber 🌸

@shimmermathlabs.com

needs more commutative diagrams

5/5/26, 2:31 pm0 reposts6 likes

Nicole Heinimann

@saltypeppermint.bsky.social

5 May

My regrettably serious take on this is that once all the prescientific productivity slop in harnesses fades away we’ll rediscover that machine checkable formal specs are kind of a nifty idea at which point LLMs will reach the final stage of every ML approach: (Proof/Program) Search

Nicole Heinimann

@saltypeppermint.bsky.social

5 May

Don’t take this as me saying LLMs are not really weird and interesting and potentially very very powerful, I’m just tired of a lot of formalism and scientific rigor LARP with mystical properties. Especially shit like auto-formalization gives me a thousand yard stare.

Amber 🌸

@shimmermathlabs.com

5 May

i think there's a chance that our very notion of "formal" will evolve into something unrecognizable to us today

Nicole Heinimann

@saltypeppermint.bsky.social

Could you elaborate?

around 2006 timeframe, i was working on formalizing different cs and math concepts. a striking thing to me was the lack of "formalization rigor" in actual papers. authors were being "formal for writing", but there are SO MANY DETAILS to get from that to actual working coq/agda etc proofs