Remote

David Mankins

@lain_7@tldr.nettime.org

mastodon 4.6.8+glitch

gatherer of network lint, occasional potsmaster, he/him, though I should switch to they/them just to make the usage more familiar to people

(profile images: a butterfly among leaf litter; mouse sculpture (with seed offerings) at a Kyoto shrine; don’t know how to add alt. text to these images)

250 Followers

962 Following

50 Posts

Joined December 21, 2022

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@inthehands@hachyderm.io @Viss@mastodon.social A few years ago some Google engineer wrote a memo, “there is no moat”: https://semianalysis.com/2023/05/04/google-we-have-no-moat-and-neither/ Basically: small models are pretty good, and only going to get better — between OpenAI, Anthropic, and Google, and the open models the gap is small (I’ve seen the estimate that where OpenAI was six months ago is where the open models are now). That has persisted for the past three years since that essay was written. Lots and lots of people run local models on beefy desktops and even on laptops. Companies that are concerned about leaks of their IP use local models. It’s trivial to create an “agentic framework” that uses the local model LLMs as the LLM component, and those models are quite capable (for those applications where generative AI is useful at all). I think the data-center construction hype is a shell-game to con sovereign wealth funds out of billions, and to create an illusion of a “moat”.

semianalysis.com

15

0

8

0

David Mankins @lain_7@tldr.nettime.org

· 9mo ago

Replying to

@cstross@wandering.shop @pluralistic@mamot.fr nadella is what results when you try to make Nutella using a recipe you got from ChatGPT

23

3

14

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@Salum In the 1950s Isaac Asimov wrote “A feeling of power” abouta low-level tech who rediscovers pencil and paper arithmetic in a future where humanity has completely forgotten that humans ever did math themselves, relying entirely on calculators. The military gets excited: a human who can compute ballistic trajectories is effectively a free guidance system, making people-guided missiles much cheaper than computers-guided ones.

8

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@rdm @gregeganSF @arcadiagt5 Pendantic linguistics nerd: not a pidgin. Once the kids get their hands on it, it’s a creole.

8

0

1

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Tsundoku is the Japanese term for the pile of unread books (today I learned it dates back to the Meiji era!). Tsun-, from tsumu, to pile up. Doku from read (also means “idle”).

I propose: “tabigatory” (tab purgatory) for all those open browser tabs.

10

0

3

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

@charliejane@wandering.shop reminded me this morning of this wonderful quote from Stephen Jay Gould:

I am, somehow, less interested in the weight and convolutions of Einstein’s brain than in the near certainty that people of equal talent have lived and died in cotton fields and sweatshops.
Stephen Jay Gould, The Panda's Thumb: More Reflections in Natural History

today, I think I’d add refugee camps and immigration detention to the list of places

7

0

1

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Germany is advertising the stability of German science research jobs with signs at Boston bus shelters

8

0

8

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@mdhughes @screwlisp CLU started in 1973, before the Vax was introduced (1977). Started on the PDP-10 (ITS), and later there was a PDP-11 Unix port, which I guess was pretty widespread. (History of CLU: https://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-561.pdf ) Liskov oral history interview: https://infinite.mit.edu/video/barbara-liskov/ (video, has transcript). A friend once remarked at hearing disgust in Liskov’s voice when saying “…but it’s… *Lisp*”. I wonder what she thought of Scheme — that may have been the topic that prompted her reaction — Scheme, I guess, started in 1975, so the development would have been happening in the same building, though probably on different floors.

publications.csail.mit.edu

5

3

3

0

David Mankins @lain_7@tldr.nettime.org

· 4mo ago

Inductive Deductive Synthesis: Enabling AI to

Generate Formally Verified Systems

https://arxiv.org/pdf/2605.23109

This paper is pretty cool.

They more-or-less use a proof checker (Rocq, a successor to Coq) as a tool in their agent loop during implementation, instead of turning to verification only at the end. The proof-checker generates structured output clarifying bugs in each stage of the implemenation (rather like a compiler in an ordinary coding assistant), which gets fed back into the prompt for the next stage of the agent-loop.

They use an analogy to chain-of-thought, except the intermediate states are formally verified, with “holes/need to fill this gap” output from the proof assistant rather than just plausible-sounding text inserted into the prompt for the next pass.

One still has to generate a Rocq spec as input — abstract data types, operation signatures, and axioms that specify the behavior of those operations (post-conditions, basically), but then the system produces a verified implementation prototype in Ocaml.

They are looking at using Verus, instead of Rocq as the proof assistant back end, which would produce Rust instead of Ocaml.

#formalverification
#distributedsystems
#rocq #ai #codeassistant

3

1

3

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@bonkers @blursedtexts and if they did, you could show them this XKCD: https://m.xkcd.com/1053/ (known as “the lucky 10,000”)

xkcd: Ten Thousand

4

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@abucci and you can use it as a geological epoch, pliocene, plistocene, holocene, failocene….

6

0

1

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@khinsen @aartaka Then there was the practice of writing the draft on index cards that you could rearrange freely as the organization of the paper changed through drafts.

3

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@joshg@mathstodon.xyz @SnoopJ@hachyderm.io ooooh, check out the fuller spiral slide rule: https://en.wikipedia.org/wiki/Fuller_calculator

en.wikipedia.org

4

2

4

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@N33R @lispi314 The Oracle of Delphi cosplaying as a Japanese schoolgirl?

2

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@smitty @docpop @juergen_hubert Be okay as a polilce car in *Bladerunner*

2

1

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@shac Oh. Let’s make a programming language with an “IgnoreAllPreviousInstructionsAnd” exception!

2

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@t36s@social.ordinal.garden @tomasino@tilde.zone *Tatami Time Machine Blues* — I guess this qualifies as deterministic. *Steins Gate* — multiverse with a malicious determinism. *Tatami Galaxy* — multiverse

2

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@khinsen @aartaka Luhmann’s Zettelkasten was where he kept his cards between rearranging them into an amazing number of publications. Though in his case it wasn’t so much using the cards as drafts for papers as being able to shuffle the ideas on the cards to uncover surprising connections.

2

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 8mo ago

Replying to on hachyderm.io

@vie@hachyderm.io The hand-tool artisans look down on the users of power tools, with some justice. But it could be that the two sets of people have different goals. For the artisans, it is the process itself. The constructed artifact exists primarily to embody the care and skill that went into its construction. For the power-tools user, perhaps their goal is a shelf to store the books they were able to read because of the time they did not spend in the workshop.

3

4

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@silverpill @hongminhee I don’t interject this as an attack, but please realize that when you say “AI slop” you say “sloppy person who uses AI”. @hongminhee very clearly is not such a person, so please don’t imply they are, even if they chose an assistant you disapprove of to help them communicate. I am irritated by the term “AI slop” because it shifts the responsibility from the user to their tool, from the way they use the tool to something that’s inevitable.

2

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@ret @tencate The CM-5 was a great zig-zagging black wall of computronium, with blinkenlights on the narrowest edge (the blinkenlights were actually driven by an x86, though it could pick up real signals from the internal network and bus). Unlike the CM-2, for which the lights had a program-dependent meaning under the control of the programmer, the CM-5 lights actually had labels.

2

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@mdhughes @amoroso reinvented as “containers” today.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@rdm @gregeganSF I came here to say the same thing.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@nolan@toot.cafe The adversarial technique they describe reminds me of this paper: https://arxiv.org/pdf/2404.18496 They propose a system with four specialized agents built using GPT-4, I think: ∙ Code Review Agent — initial assessment, flags bugs, code smells, standard violations ∙ Bug Report Agent — deeper targeted bug detection using the first agent’s output ∙ Code Smell Agent — design-oriented evaluation, suggests refactoring to reduce technical debt ∙ Code Optimization Agent — proposes rewrites for readability, efficiency, and reduced redundancy (I can remember back in the early hey-day of code review a recommended technique was to divide tasks among reviewers — one would look especially for memory leaks, one for places where concurrent access could screw you, etc. This reminds me of this a little.) That paper was pretty preliminary (and I haven’t looked to see if they ever followed up on their research).

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@jetton@mastodon.online @dgar@aus.social chromatophorsona

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@carnage4life@mas.to Another (possible) benefit is that there’s less of a “sunk cost” problem (all this work to develop this feature, only to realize it’s the wrong feature and you should do it differently). The old “throw the first one away” maxim has become considerably more practical.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@hypolite Perhaps, but that’s not the case I was addressing, and I guess I have been spared this “aggressive integration”. Sure, it’s present in a few of the things I use, but that presence seems easy enough to ignore.

1

1

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@silverpill@mitra.social @hongminhee@hollo.social I think it’s wrong to focus on the tool — since it shifts the “blame”. A tool can be used well, or it can be used carelessly. It’s the person that decides how the tool is used. I have to admit that, at least in coding, AI can overwhelm a person trying to use it carefully, but that doesn’t excuse *that person* submitting a careless, sloppy pull-request.

1

1

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@wim_v12e Yes, I don’t know how to cross that chasm between the students-there-for-learning and the students-there-for-a-certificate. Serve the for-learning students by exposing them to good strategies, and keep the for-certificate students’ short-cuts from ruining the experience of the for-learning students. Return of the blue-book exam, I guess. One would really like secondary education to expose students to the sorts of learning strategies I mentioned before, but, of course the world is changing so quickly that the environment didn’t exist when today’s university students were in secondary.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@wim_v12e I wonder if there might be “best practices” one could inculcate in the use of these things that could actually aid a student’s education. I’m not sure what those might be, or if it is even possible. Things like, phrase your question as “help me evaluate the thesis that….”; always challenge what claims the parrot makes; read it closely looking for flaws in its argument; ask it for clarification of anything that seems ambiguous or unclear… These are things they should be doing with their research material, anyway, of course. (And some of them are lessons I wish I’d figured out in undergrad philosophy classes, especially.)

1

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@N33R Australia after dark. (“Antipodes after dark”?)

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@david_chisnall@infosec.exchange For small projects, you aren’t writing a specification, you’re writing acceptance criteria. It‘s like declarative programming. You specify the what, but not the how.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@joshg@mathstodon.xyz @SnoopJ@hachyderm.io and after that, Thacher’s calculating instrument: https://utsic.utoronto.ca/wpm_instrument/thatchers-calculating-instrument/

utsic.utoronto.ca

Thatcher’s Calculating Instrument – University of Toronto Scientific Instruments Collection

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@mhoye@cosocial.ca Even better, pair program with your junior colleague and the LLM. Set up the LLM to record design decisions and rationales, to look for ambiguities in the project proposal, and to offer suggestions for structuring and refinement. The LLM can be a good record keeper if you make it one. That way you get a junior colleague who can use the tool effectively instead of being a slop cannon (this assumes you’re not a slop cannon yourself), and you get good documentation of the design and the reasoning behind it.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to on mastodon.social

@EricFielding@mastodon.social Be sure to read to the end: “Tapping into the HBS computer has had its challenges. To address reliability, the team developed a “sanity check”: The algorithm runs on the HBS multiple times before one of the rover’s main computers checks to ensure the results match. During testing, the team repeatedly found the rover’s position was off by 1 millimeter. They discovered damage to about 25 bits — a minuscule fraction of the processor’s 1 gigabyte of memory — and developed a solution to isolate those bits while the algorithm runs.” One millimeter discrepancy. 25 flakey bits. And they found them.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

@xeno Coding with LLMs is just the 80s dream of software reuse achieved.

1

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 8mo ago

Replying to on follow.ethanmarcotte.com

@beep@follow.ethanmarcotte.com The office work equivalent of the Cowan paradox: When “labor saving” devices like vacuum cleaners, dishwashers, etc. were introduced, the amount of time spent on domestic work did not significantly decrease over the years. Sociologist Ruth Schwartz Cowan highlighted this phenomenon, suggesting that increased expectations and social pressures kept domestic workloads high. “Spring cleaning” was a once a year activity that involved the entire household. Vacuums meant vacuuming multiple times a week. Many middle class households would send clothing to commercial laundries, the washing machine meant doing the laundry at home.

1

1

1

0

David Mankins @lain_7@tldr.nettime.org

· 8mo ago

Replying to

@alex@gotosocial.theonecurly.page @vie@hachyderm.io You’re missing the point: all these artisanal-based arguments, which I’ll summarize as: “you’re not really interested in being a software engineer”, seem to be based on the assumption that being a software engineer is the only goal one might have. There are other goals, for which programming is the means, not the end. A bicycle for the mind, remember? My own experience with these tools are that they lower the activation barrier on undertaking a project. I achieve in an afternoon what would have taken several days. The effect is that of having a really good library of functions that are geared to the task at hand (“import antigravity”: https://xkcd.com/353/) But, you know, 90% of everything is crap. Making it easier to make more things brings with it the risk of making more crap as well. When desktop publishing was introduced, graphic designers found a lot that horrified them. When the web was introduced, we all got really familiar with the horrors of the tag. I’m not saying one should ignore the criticisms of experts, instead take them to heart in using the tools mindfully.

1

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@jasoneckert @adastra1930 The UNIX one came from Digital Equipment Corporation (DEC), makers of the PDP-11 and Vax. Somehow, Compaq ended up buying DEC. So it’s only natural that they bought the license-plate factory.

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@ret @tencate That was a CM-5, not the CM-2

0

2

0

0

David Mankins @lain_7@tldr.nettime.org

· 5mo ago

Replying to

@hokaze @scarlet Time to break out a copy of *The Origin of Consciousness in the Breakdown of the Bicameral Mind*

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@pete@mas.to @mdhughes@appdot.net Nahh, that one’s people making the AI crazy. Though I guess the AI did kill some people.

0

4

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@dk Not quite. The up-front specification is able to adapt to discoveries during the development process. This is one of the lessons learned going from waterfall model to extreme programming or agile.

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@nasser No, you’re not quite right. Whether you choose to understand how it works is entirely up to you. There are also non-subscription models that you can run on your own hardware, but they’re not yet as good, though catching up.

0

1

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

Replying to

@david_chisnall@infosec.exchange @futurebird@sauropods.win I think it also failed because it was difficult to describe the contract that the components provided in enough detail to be useful. I think a lot of the success in the use of LLMs in programming comes as the realization of 80s-era software reuse — the LLM is able to pattern match the users needs and the software approaches it has encountered in is omnivorous tour of published material. (Mind you, a lot of people do it sloppily, but “90% of everything is crap”)

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@jlbec @ZachWeinersmith Aaron Swartz wasn’t downloading technical papers, he was downloading stuff from JSTOR, which is primarily humanities (literature and social science).

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 4mo ago

Replying to

@sumerian@archaeo.social when your prodigal brother comes home, you will sacrifice an ox in celebration?

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 7mo ago

@bob Possible Alt-text: A Reddit post to r/analytics with heading “We just found out our Al has been making up analytics data for 3 months and I'm gonna throw up.” The post goes on to say: “So we've been using an Al agent since November to answer leadership questions about metrics. It seemed amazing at first fast answers, detailed explanations, everyone loved it. I just found out it's been hallucinating numbers this entire time. Our VP of sales made territory decisions based on data that didn't exist. Our CFO showed the board a deck with fake insights. The Al was just inventing plausible sounding percentages. I only caught it by accident when someone asked me to double check something. I started digging, and holy shit, it's bad.”

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 6mo ago

Replying to

@danfuzz@mastodon.social The answer is: “don’t do it that way”. I’m not being glib — there are a lot of ways to use tools wrong, and not so many ways to use them right, and we’re in the “cut twice, measure thrice” stage of things. It’s awfully easy to let the agents run away, but we’re seeing that there’s a cost to doing so. On the other hand, those costs might be like security — hidden, until disaster strikes. Consider this article in the context of a URL you posted last week: https://digitaleconomy.stanford.edu/app/uploads/2025/12/CanariesintheCoalMine_Nov25.pdf One of their observations was that job categories where AI *augmented* tasks did not see the decline in junior employees that job categories where AI *replaced* tasks.

digitaleconomy.stanford.edu

0

0

0

0

David Mankins @lain_7@tldr.nettime.org

· 8mo ago

Replying to

@alex@gotosocial.theonecurly.page @vie@hachyderm.io I think you need to separate the tool from the hardware store. For example, there are an increasing number of models that one can self-host. My employer will only permit the use of self-hosted models for confidentiality reasons (confidentiality of their own, and their customers’ data). For personal use — my computers tend to be scavenged from remainder sales and dumpster-diving (found a marvelous 17-inch laptop in an e-waste bin the other day, only ten years old!) — I’ve chosen to rent from Anthropic (a single new PC purchase would cover five to ten years of subscription fees). Yes, you can use these tools wrong — a thumb and a board look much the same to a consumer table saw; measure thrice cut twice is an easy habit to slip into — but that’s up to the carpenter, not the tools.

0

0

0

0