Types are best, period. Whether they are native or hints doesn't really matter for the agent, what matters is the interface contract they provide.

▲

simianwords 3 hours ago | parent [-]

I don’t get this argument because if we put the effort to get it typed, we don’t get one of the best benefits - performance.

▲

maleldil 3 hours ago | parent | next [-]

But that's not the argument here. Python type hints allow checking correctness statically, which is what matters for agents.

▲

simianwords 3 hours ago | parent | next [-]

Yes then you might as well use some other language that uses types but also gets you performance. I agree the ecosystem is missing but hey we have LLMs now

	▲	solumunus 3 hours ago \| parent [-]
		Performance isn’t the only important metric. There are other pros to weigh. For many apps a language might be performant enough, and bring other pros that make it more appealing than more performant alternatives.

▲

wincy 2 hours ago | parent | prev | next [-]

That’s what makes types easier for me, too, so that makes sense.

▲

9rx 2 hours ago | parent | prev [-]

> Python type hints allow checking correctness statically

Not really. You can do some basic checking, like ensuring you don't pass a string into where an integer is expected, but your tests required to make sure that you're properly dealing with those integers (Python type hints aren't nearly capable enough to forgo that) would catch that anyway. The LLM doesn't care if the error comes from a type checker or test suite.

When you get into real statically typed languages there isn't much consideration for Python. Perhaps you can prompt an LLM to build you an extractor, but otherwise, based on what already exists, your best bet is likely Lean extracted to C, imported as a Python module. Easier would be to cut Python out of the picture, though.

If you are satisfied with the SMT middle-ground, Dafny does support Python as a target. But as the earlier commenter said: Types are best.

▲

shadowgovt 3 hours ago | parent | prev [-]

The best benefit depends on your problem domain.

For a lot of the business world, code flexibility is much more important than speed because speed is bottlenecked not on the architecture but on the humans in the process; your database queries going from two seconds to one second matters little if the human with their squishy eyeballs takes eight seconds to digest and understand the output anyway. But when the business's needs change, you want to change the code supporting them now, and types make it much easier to do that with confidence you aren't breaking some other piece of the problem domain's current solution you weren't thinking about right now (especially if your business is supported by a team of dozens to hundreds of engineers and they each have their own mental model of how it all works).

Besides... Regarding performance, there is a tiny hit to performance in Python for including the types (not very much at all, having more to do with space efficiency than runtime). Not only do most typed languages not suffer performance hindrance from typing, the typing actually enables their compilation-time performance optimizations. A language that knows "this variable is an int and only and int and always an int" doesn't need any runtime checks to confirm that nobody's trying to squash a string in there because the compiler already did that work by verifying every read and write of the variable to ensure the rules are followed. All that type data is tossed out when the final binary gets built.