Yaron (Ron) Minsky

@samth @ArjunGuha @ShriramKMurthi The point being that the hard structure of the types helps you figure out where you should dig deeper. But source files are still useful.

@samth @ArjunGuha @ShriramKMurthi Is it? I use types for exploration and I read source files. Agents might do the same

So, I really want someone to do a study on the effectiveness of types for agents. Studying the same question with humans is absurdly expensive, but agents provide a new way of asking the question. Is anyone working on this?

@jameskjx For sure. But it's an interestingly related question!

@yminsky studying this with agents doesn't provide a new way of asking the question --- rather it's a way of asking (or at least starting to answer) a *different* question. but again: remember you a studying agents not (just) type systems. most likely mostly studying the agents.

@samth @difficultyang Maybe, though, I worry that the measurements of success that are used in those benchmarks are fairly weak. I'd be interested in some more time intensive, human evaluations of the quality of the results.

@difficultyang @yminsky I think the success rate at "one shot" (with an agent) on real programming tasks in the SWE-bench vein is the right metric.

@difficultyang I agree that a mere lack of type errors is not an interesting goal. I would think that it would be reasonable to measure the speed at which a hard task is completed, as well as the defect rate of the resulting code.

@yminsky Let's define the first order question then. "Well" is very underspecified. "Doesn't have type errors" is too easy (or too hard? Mumble mumble math proofs). Is our goal token efficiency? Latency? Success rate at the one-shot task?

@difficultyang But that's still an empirical question I'd love to see validated!

@difficultyang But I suspect that types do make agents more useful when humans are doing a good job with design

@difficultyang But... You know as well as anyone that types can prevent a wide variety of bugs! So why an I telling you this?

@difficultyang XSS and SQL injection attacks can be prevented as well.

@ShriramKMurthi Woohoo! Looking forward to the results.

@yminsky Yes. Two studies being designed.

@difficultyang That's not a crazy outcome, but it's pretty surprising. I think feedback is super important when you get beyond toy problems. And I think it's really hard to get similarly good results by just improving the prompts.

@difficultyang Meaning that the variants in results between different prompting approaches and different ways of setting up the agentic harness will dominate differences in the kinds of feedback you provide to the model?

@agniv_s More or less

@yminsky Like, your question is "given a more general SWE-BENCH style of benchmark, and giving an agent a typechecking tool that it can use, does this meaningfully improve results?"

@SMT_Solvers @headinthebox @NousResearch Python is a tough language to answer this question with because the type feedback is comparatively weak.

@yminsky @headinthebox however you can do it with @NousResearch Hermes. Have it build coreutils in Python without type annotations, then do it with type annotations. Which is faster after a few runs?

@agniv_s The core question I'm interested in is whether an agent given a type system will generate better results, more quickly than one without.

@yminsky could you clarify what the effectiveness of types for agents means? like, if i give an agent access to a sandbox with a strong compiler, how it reacts to the compiler feedback? or agent-as-compiler, see what types of types it creates when taking in a prompt?