Just recently I heard that they can donate to “typed languages” too, a donation to one language does’t preclude other donations, and given their cash injections they have a few $1.5m’s to spare.
For any programming really, but I think Python got big due to
a) the huge influx of beginners into IT,
b) lots of intro material available in Python and
c) having a simple way to run your script and get feedback (same as PHP)
I say that as someone urging people to look beyond Python when they master the basics of programming.
Python has a terseness that is hard to rival. I think that was a major selling point: its constructs and use of whitespace mean that a valid Python program looks pretty close to the pseudo-code one might write to reason out the problem before writing it in another language.
Python doesn't require you to understand monads to write useful Python.
To be clear: Haskell is great, but its entire vibe (lazy evaluation, pure functions) is entirely different from what Python's about. Someone who knows C++ or Java has a much bigger gap to jump to pick up Haskell than to pick up Python.
> Someone who knows C++ or Java has a much bigger gap to jump to pick up Haskell than to pick up Python.
True, they are all imperative c-style languages.
> Python doesn't require you to understand monads to write useful Python.
If that is the concern I would recommend anyone interested to dabble with F#. Part of its design philosophy is to keep the complexity out wrt type systems. It offers a vast vetted library¹, better dependency management², it is truly multi-paradigm (imperative, functional and oop), vastly better performance, and it is strongly typed without requiring type annotations³.
I know I am not going to sell it to monogamous devs, but those that are open minded should give it a try.
___
¹ This is something people will start to appreciate once they get serious about the risk of supply chain attacks.
² Python developers feel they are doing fine with pip or uv, at least in my experience, but then I find they haven't dealt with package mgmt in alternative languages.
³ Types in python are a hack, bolting on something afterwards will not reach what is possible with a language that has been designed with types as core element.
Python type hints are static - at the moment, they are advisory only, but there is an obvious route forward to making Python an (optionally) fully statically typed language by using static type checking on programs before execution.
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.
> 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.
I think you're underestimating the current state of the Python type system. With Python 3.12 and pyright or mypy in strict mode, it's very reliable, and it makes those kinds of tests unnecessary. This requires you to fully buy into the idea, though, with 100% of your codebase statically typed and using only typed libraries, unless you're comfortable writing wrappers.
It's not Rust-level, but I'd argue it's better than C or Go's type systems.
The comparison with Rust and not something like Lean, Rocq, or Idris is telling. Rust's type system is not much better than Python's, still requiring tests for everything.
These partial type systems cannot replace any actually useful tests. I'll grant you that testing is the least understood aspect of computer science, leading to a lot of really poorly conceived tests out in the wild. I can buy that those bad, useless tests can be replaced — albeit weren't actually needed in the first place.
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
I don't understand why you keep bringing up performance. If you're considering using Python, as many projects are, performance is obviously not a concern.
Python is a good language. Its ecosystem is rich, and I find it very productive. I want to use it, but I also want as much static analysis as possible, so I use ruff and pyright.
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.
It's true; mypy won't make your Python faster. To get something like that, you'd want to use Common LISP and SBCL; the SBCL compiler can use type assertions to actually throw away code-paths that would verify type expectations at runtime (introducing undefined behavior if you violate the type assertions).
It's pretty great, because you can run it in debug mode where it will assert-fail if your static type assertions are violated, or in optimized mode where those checks (and the code to support multiple types in a variable) go away and instead the program just blows up like a C program with a bad cast does.
I'd say most of us who prefer Python (a pretty significant number given it's the most popular language out there) don't care that much about performance, as today's machines are pretty fast and the main bottlenecks aren't in the language itself anyway. What we care about is usability/friendliness so we ourselves can iterate quickly.
If your code is talking to an LLM, the performance difference between rust and python represents < 0.1% of the time you spend waiting for computers to do stuff. It's just not an important difference.
Why is this getting downvoted... it is true. Also it is true that dynamic languages (like Ruby ;) and Python) are more efficient with tokens, like significantly then types like C, C++ or such. But Javascript and Typescript are using twice the tokens of Ruby for example and Clojure is even more efficient, obviosly I would add.
AFAICT Python basically is a [statically-]typed language nowadays. Most people are using MyPy or an alternative typechecker, and the community frowns on those who aren’t.
> Most people are using MyPy or an alternative typechecker, and the community frowns on those who aren’t.
That's not like a widespread/by-default/de-facto standard across the ecosystem, by a wide margin. Browse popular/trending Python repositories and GitHub sometime and I guess you can see.
Most of the AI stuff released is still basically using conda or pip for dependencies, more times than not, they don't even share/say what Python version they used. It's basically still the wild west out there.
Never had anyone "frown" towards me for not using MyPy or any typechecker either, although I get plenty of that from TS fans when I refuse to adopt TS.
I think in the case of TS, it's more that JavaScript itself is notoriously trash (I'm not being subjective; see https://www.destroyallsoftware.com/talks/wat), and TypeScript helps paper over like 90% of the holes in JavaScript.
Python typed or untyped feels like a taste / flexibility / prototyping tradeoff; TypeScript vs. JavaScript feels like "Do you want to get work done or do you want to wrap barbed wire around your ankle and pull?" And I say this as someone who will happily grab JS sometimes (for <1,000 LOC projects that I don't plan to maintain indefinitely or share with other people).
Plus, TypeScript isn't a strict superset of JavaScript, so choice at the beginning matters; if you start in JS and decide to use TS later, you're going to have to port your code.
Typed Python vs untyped Python is literally the same as TS vs JS, don't let others fool you into thinking somehow it's different.
> TypeScript helps paper over like 90% of the holes in JavaScript
Always kind of baffles me when people say this, how are you actually programming where 90% of the errors/bugs you have are related to types and other things TS addresses? I must be doing something very different when writing JS because while those things happen sometime (once or twice a year maybe?), 90% of the issues I have while programming are domain/logic bugs, and wouldn't be solved by TS in any way.
I mean, I'm one of the fools who would fool you into thinking it's different, since I use all four languages. ;)
I can just skip the mypy run if I want to do untyped Python. I can't skip adding types if I'm writing TypeScript in most contexts; it's not valid TypeScript syntax. Conversely, I can't add types to JavaScript; it's not valid JavaScript syntax (jsdoc tags and running a static checker over that being a different subject, and more akin to the Python situation).
> how are you actually programming where 90% of the errors/bugs you have are related to types and other things TS addresses
It's the things in the "wat" video. JavaScript, in general, errs on the side of giving you some answer when you try and do something very unusual with types (like add a boolean to a number or a string to an array) over taking a runtime error. TypeScript will fail to typecheck in most of the places where those operations are techincally correct but surprising as hell in the wrong way unless you explicitly coerce the types to match up.
It's a funny video, still after 15 years of seeing it, I'll give you that. But the number of times I'm bothered by accidentally triggering those scenarios in real-life? Could probably count that on one hand.
I also give you that TypeScript helps beginner JavaScript developers a ton, and that's no easy feat by itself, just because of those things you mention. Once you build up intuition about how things work in JavaScript though, those sort of bugs should stop happening though, otherwise I'd say you aren't really learning the language.
> Never had anyone "frown" towards me for not using MyPy or any typechecker either
I’ve seen it many times. Here’s one of the more extreme examples, a highly-upvoted comment that describes not using type hints as “catastrophically unprofessional”:
But yeah, that's reddit, people/bots rejoice over anything being cargoculted there, and you really can't take any upvote/downvote numbers on reddit seriously, it's all manipulated today.
Don't read stuff on reddit and use whatever you've "learned" there elsewhere, because it's basically run by moderators who try to profit of their communities these days, hardly any humans left on the subreddits.
Edit: I really can't stress this enough, don't use upvotes/likes/stars/whatever as an indicator that a person on the internet is right and has a good point, especially not on reddit but I would advice people to not do so on HN either, or any other place. But again, especially on reddit, the upvotes literally count for nothing. Don't pick up advice based on upvoted comments on reddit!
Generally you only get frowned at if you're not using type hints while contributing to a project whose coding standards say "we use type hints here."
If you're working on a project that doesn't use type hints, there's also plenty of frowning, but that's just because coding without a type checker is kind of painful.
> Generally you only get frowned at if you're not using type hints while contributing to a project whose coding standards say "we use type hints here."
Yeah, that obviously makes sense, not following the code guidelines of a project should be frowned upon.
It's a pretty nice best-of-both-worlds arrangement. The type information is there, but the program still runs without it (unless one is doing something really fancy, since it does actually make a runtime construct that can be introspected; some ORMs use the static type data to figure out database-to-object bindings). So you can go without types for prototyping, and then when you're happy with your prototype you can let mypy beat you up until the types are sound. There is a small nonzero cost to using the types at runtime (since they do create metadata that doesn't get dropped like in most languages with a static compilation step, like C++ or TypeScript).
I can name an absolute handful of languages I've used that have that flexibility. Common LISP comes to mind. But in general you get one or the other option.
> It's a pretty nice best-of-both-worlds arrangement
It’s also a worst-of-both-worlds arrangement, in that you have to do the extra work to satisfy the type checker but don’t get the benefits of a compiled language in terms of performance and ease-of-deployment, and only partial benefits in terms of correctness (because the type system is unsound).
AFAIK the Dart team felt this way about optional typing in Dart 1.x, which is why they changed to sound static typing for Dart 2.
Without dependent typing, it's the worst of all worlds anyway. You have to express types, but they aren't expressive enough to not have to also express the same in tests, leaving this weird place where you have to repeat yourself over and over.
That was an okay tradeoff for humans writing code as it enables things like the squiggly line as you type for basic mistakes, automatic refactoring, etc. But that stuff makes no difference to LLMs.
