Recently had to touch a Python project at work. Just setting up the editor needed me to use 2-3 tools out of: pyright, basedpyright, ruff, ty, mypy, and possibly other tools I'm forgetting that kind of do the same thing but throw errors in different parts of the codebase.
Also, for some reason Optional[T] became deprecated, just as the ecosystem finally embraced types ~3 years ago.
In fact, one my company's greenfield projects decided to use TypeScript instead of Python for the [surprisingly] more consistent tooling, and the fact that the big LLM providers all have official TypeScript SDKs anyway. Also, for agentic coding, LLMs don't seem noticeably worse at TypeScript than Python.
My experience can be summarized as:
- for some reason we need 2-3 static analysis tools just for typechecking
- no tool understands each other's comment directives
- each tool reports a different error in your codebase
- even big libraries (e.g. matplotlib) make half their functions return Any
- you'll be tempted to silence the "partially unknown type" warnings, and you'll have to do it for each tool that's running.
It doesn't mean "we believe reality works this way". It means "at extremely small scale, probabilistic models from QM best predict the behavior of electrons".
Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it.
Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago.
I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
Many organizations, surprisingly, still do things like using Kubernetes with TLS terminated at the ingress. In that case, you just need the splitter in the same network as the nodes hosting the ingress controller. Or inspect the unencrypted traffic within the cluster.
It takes a non-trivial amount of work to set up a service mesh (and mutual TLS between services), so many k8s clusters end up with unencrypted traffic inside the cluster network.
1. TypeScript doesn't aim to have a sound type system. i.e. there may be things the type system accepts that are actually unsafe.
2. this is more of an issue with mutation. If those properties were marked `readonly`, then the assignment of y.a wouldn't work at all. You can also encapsulate mutation behind functions with your intended types.
I tend to write TypeScript in a "functional" or "immutable" way, and in this case, most soundness issues come from things like array index access, which can't really be solved without dependent types anyway.
With that said, TypeScript still gets one quite far *despite* soundness not being a goal of the type system. The problem is that writing imperative, mutable code will make you go through (intentionally!) unsound covariance of types. Similar issues exist for code with side effects, since TypeScript has no way to encode effects in the type system. This is why some language communities settle on ideas like "functional core, imperative shell", where the ultimate goal is absolute minimum amount of code involved in side effects and mutation, while everything else is designed to be easy to test (and, ideally, expressible with a sound subset of your type system).
There is a mobile game I know of that had an outage as a result of a GCP service outage. That is the only time I've noticed GCP outages.
With that said, I would not say few companies rely on GCP. Search for "GCP" in this month's HN hiring thread. There are 23 hits, more than Azure's 21. AWS has 90 hits, which I guess shows its sheer dominance in the startup space. But these figures more or less agree with my intuition of the major clouds being AWS/GCP/Azure.
Pretty much every mountainous region in the mainland of Japan, except for Chiba prefecture, has bears. Most people do not live in the mountains, which is why bear sightings tend to be limited to the areas with (a) significant human population, (b) proximity to mountains.
Since the OP stated they used DeepSeek V4 Flash for generating a lot of the code, I decided to check whether there were any outdated dependencies. In my experience, with Rust projects, if you do not instruct models (even Claude 4.7 Opus) to use `cargo add` instead of manually editing the Cargo.toml, you will almost certainly get out-of-date dependencies added to your project.
Manually checking the dependencies used by this project, I was pleased to see they are all the latest version. That doesn't mean there are no issues lurking in transitive dependencies, of course.
As for getting an LLM to review the code, I think we can get all opinionated very fast. For instance, when I was eyeballing the code, some of the enum methods converting to/from strings made me think "this could've been a single #[derive] with strum." That would make the code in provider.rs a lot more concise, at the cost of importing one crate (with no dependencies!)
Lastly, for fun, I decided to get DeepSeek V4 Pro (with Max thinking) to "audit" the codebase. The output mentioned no obvious signs of hidden telemetry, but it did note that the project sets the panic handler to "abort", which I have strong opinions on... Presumably the OP wanted to avoid linking against libunwind to save a few kilobytes of binary size, but now you have a binary that immediately aborts and doesn't give the user a stacktrace of what just crashed. I would rather have a ~50 KiB larger binary if it means getting useful debug info during a panic. Additionally, if there are async tasks that panic, they can't be recovered to display a generic error message; instead the whole process just aborts.
I noticed borkdude posted this thread *and* he is listed as a contributor for this release.
For the longest time, I recall the opposition to async/await support being twofold:
1. adding support would require deep changes across the CLJS compiler (theller, creator of shadow-cljs, once tried and concluded this)
2. macros from libraries like Promesa provided similar convenience
There were some other arguments brought up at the time (e.g. just use core.async, expression-oriented languages aren't a good fit with async/await, etc.), but they were usually specific to one person rather than something you'd see repeated in forums.
In the Clojurians Slack, borkdude once stated he wasn't convinced it'd be impractical to add support. It seems that he eventually took the time and made it happen. Extremely thankful for that.
MPEG-2 TS is a container. H.264 is a coding specification. They are totally different things.
One can find MPEG-2 TS in surprising places (see: DOCSIS encapsulating Ethernet frames into TS packets).
If I had to guess why MPEG-2 TS, it'd probably be the for the fact it's a well-supported streaming format in both hardware and software. If you tried using QuickTime or MPEG-4 containers, you'd have to rely on hacks like ensuring the moov atom preceeds mdat.
Matroska may be worth considering (especially the subset used by WebM to make it stream-friendly and quicker to seek), but no idea how widespread hardware support is for (de)muxing that.
For what it's worth, Kine (software that k3s uses to replace etcd with SQL databases) implements etcd watches on SQLite through polling[1]. The reason being that SQLite does not offer NOTIFY/LISTEN like MySQL and Postgres do. Ironically, Honkey attempts implementing NOTIFY/LISTEN through polling.
k3s has been running on my home server for about three years now (using the default SQLite backend), and there doesn't seem to be excessive CPU usage despite dozens of watches existing in the simulated etcd. Of course, this doesn't say much about Honker, but it's nonetheless worth pointing out that sometimes the choice of database forces one towards a certain design.
Most of the rail has get around mountainous, uneven terrain subject to earthquakes, strong winds, and heavy rain. California should be able to build rail parallel to the I-5, a long, flat terrain without extreme weather or strong earthquakes. The problem seems to be a political one, not an engineering one. In fact, if the Interstate Highway System did not already exist, I doubt the U.S. today would be able to accept and complete it.
> one long line with a few branches
I currently live in Japan, and that does not really match what I've observed. There are three distinct railway companies in my area (JR, Tokyu, Yokohama Municipal Subway), each with their own dedicated rail, trains, power supply, etc.
The situation is more like "a disjoint union of graphs, where some of the graphs are connected".
At my current job, I sometimes set up a Nix shell with the GitHub CLI, since that let's Claude Code associate a feature branch to a pull request. The LLM can then retrieve PR description, workflow results, review comments, etc.
Also, I believe GitHub Actions cache cannot be bulk deleted outside of the CLI. The first time I [hesitantly] used the gh CLI was to empty GitHub Actions cache. At the time it wasn't possible with the REST API or web interface.
> what do these LLM clichés look like in Japanese?
Besides text reading like a machine translation, the tell-tale signs often involve things like:
- itemized lists (I know, it's ironic that I'm using them here)
- frequent use of conjunctions
- use of demonstratives that feels redundant
- full-width colons, especially in titles
- subheadings that always end in abstract nouns
- bold text, especially at the beginning of a line
The demonstrative bit may be hard to express, but to give you an idea: when communicating in Japanese, words that can be understood from context may be omitted. Explicitly writing out words understood from context can sometimes make a sentence sound redundant.
Before LLMs were widespread, SEO spam in the Japanese net tended to be affiliate sites with predictable, template paragraphs. I get reminded of those sites whenever GPT starts a response with 「結論から言うと、〇〇」, since that's exactly how those affiliate sites wrote back in the day.
The intent is to have a proof of some proposition. The Lean runtime crashing doesn't stop the lean-zip developers from formally modelling zlib and proving certain correctness statements under this model. On the other hand, the Lean kernel having a bug would mean we may discover entire classes of proofs that were just wrong; if those statements were used as corollaries/lemmas/etc. for other proofs, then we'd be in a lot of trouble.
When I see a title transitioning from "Lean said this proof is okay" to "I found a bug in Lean", I'm intuitively going to think the author just found a soundness (or consistency) issue in Lean.
Yeah, the title made me think the author found a bug in the Lean kernel, thus making an invalid proof pass Lean's checks. The article instead uncovers bugs in the Lean runtime and lean-zip, but these bugs are less damning than e.g. the kernel, which must be trusted to be correct, or else you can't trust any proof in Lean.
> What's preventing Japanese engineers from doing the same?
The fact they don't really need it in their life (or job). English is definitely necessary if you work service jobs in Tokyo (to deal with tourists), but not much anywhere else.
Japanese is one of a handful of languages where one can complete a postdoc entirely within the language. Many languages are not like this. e.g. in the Phillipines, STEM subjects are almost entirely taught in English, since Tagalog simply doesn't have words to describe most of the concepts. The result is something like 90% of the coursework being in English, with random Tagalog words mixed in. The concept is called "Taglish" if I recall correctly.
This is unnecessary in countries like Japan, China, South Korea, etc. If you're applying to a graduate school in Japan (or China, or Korea), expecting to receive education in English is actually the edge-case, not the expectation.
Also, at least in my company, there is an interesting trend where people are deciding learning English isn't really necessary since AI translation has gotten "good enough" for most use cases.
I wonder how the figures look for countries outside of the United States.
For what its worth, I ended up getting a tech job in Japan instead. Ironically, the requirements at U.S. startups are much higher, and U.S. startups fit the stereotype of Japanese work culture more than Japanese companies nowadays.
Also, for some reason Optional[T] became deprecated, just as the ecosystem finally embraced types ~3 years ago.
In fact, one my company's greenfield projects decided to use TypeScript instead of Python for the [surprisingly] more consistent tooling, and the fact that the big LLM providers all have official TypeScript SDKs anyway. Also, for agentic coding, LLMs don't seem noticeably worse at TypeScript than Python.
My experience can be summarized as:
- for some reason we need 2-3 static analysis tools just for typechecking
- no tool understands each other's comment directives
- each tool reports a different error in your codebase
- even big libraries (e.g. matplotlib) make half their functions return Any
- you'll be tempted to silence the "partially unknown type" warnings, and you'll have to do it for each tool that's running.