kccqzy

I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.

I respectfully disagree. Single-person projects that are not commercially motivated always have the risk of abandonment, regardless of how polished they seem. Depending on the problem itself, I could very well get bored after 8 minutes of effort, or 8 months of work. Some of my personal projects had a lot of polish because I really cared; I abandoned them because I stopped caring.

(Also, adding polish was a great procrastination activity when you did not want to work on more important tasks.)

Hey world, here is a thing you should all care about and invest in.

I think this is where our mentality differs the most. I never requested the world to care about my projects, which is why I did not feel any weight of responsibility when I abandon my projects.

Nah. I made plenty of software and then abandoned them because I lost interest in them. My GitHub is already a fairly large collection of my own abandoned software, and there are 10x more on my PC that I never bothered to upload to GitHub.

Easy abandonment is always there.

I completely agree with you, but I do think that these teens do not have good opsec around these photos. It’s like the revenge porn problem but way worse. A teenager sending a nude selfie to a friend who then later shared these images non-consensually is a much bigger problem than if the same thing happened to adults.

I don’t have any ideas for a solution, but I suspect that the heightened focus on CSAM is really compensating for the fact that we don’t have solutions for revenge porn.

And sometimes optimizing for constraints happen because someone from above (perhaps someone with a title of Director who doesn’t actually write code) imposed their constraints on the team without understanding the ramification of these constraints. It takes a manager with very good people skills and/or very good writing skills to persuade that someone to drop their constraints.

The New York Times is actually part of the reason why Google’s reputation went downhill. Somewhere around 2010–2015, the NYT and other traditional newspapers finally woke up and realized that their traditional job of disseminating information to the masses had been supplanted by a new generation of tech companies including Google and Meta. So the NYT and other newspapers soured their opinions around the time. If you read the NYT, just like many intellectuals do for priding themselves for reading a serious publication, your opinions of Google would have drastically changed around that timeframe too.

However among my circle of friends (who are in general not readers of the NYT), the main reason Google became hated was shutting down products (starting from Reader, culminating in Inbox) and launching duplicative products (how many chat apps did Google have). The hate had absolutely nothing to do with surveillance capitalism. If anything people hated Meta for that; Google’s role in surveillance capitalism was basically nil compared to Meta.

It’s just not possible. FWIW my employer did not get onboard to the Cloud trend and continued to buy hardware for in-house data centers. But the kind of hardware needed to run sophisticated models are simply not for sale at the volume needed by a single company.

National parks in California are indeed amazing. One time during a group trip to Death Valley, people were so amazed by the night sky that half decided to sleep outside the tents just to experience falling asleep while looking at the stars.

Even Fable doesn't fully follow instructions.

But Bun did not even release a new version of Bun written in Rust yet. It was still a canary version.

Bun does not have its own JIT compiler. Bun uses JSC made by Apple. So your blame should be directed to Apple.

And I can believe you because I’ve seen JavaScript-heavy Safari tabs crash.

That blog post doesn’t make sense to me at all. The author is going from full modern Haskell (since he mentioned Servant and Beam, you could tell almost every file uses dozens of GHC extensions beyond what Haskell2010 gives you) to Python with dynamic types. He could instead rewrite the Haskell to use less modern type system features and get so much faster compilation speed.

Also GHC has an interpreter. It powers the REPL. No need to compile everything if you’re just experimenting. I do find that in the Haskell world the REPL is criminally underused compared to Python.

And the rest of your comment doesn’t make sense; this shop is rewriting their infra (not UI) from Haskell to Python.

Although Coros watches are fast, the Coros DURA bike computer is pretty slow when re-rendering maps. Naturally, companies can still choose between how fast the CPU is versus how long the battery life is (100+ hours on the Coros DURA I believe).

You just haven’t worked on tasks that are complicated enough. Occasionally it took more than 1M tokens just to come up with a plausible plan.

Personally I find using /rewind judiciously is better than using /compact. The latter essentially gives you no control of what details to discard, but the former at least has coarse-grained control.

Banks and financial institutions are the same. If they haven’t issued you a monthly/quarterly statement yet, they can just apologize and tell you the numbers are wrong please wait for the statement. But it is a major issue if an actual statement has the wrong numbers.

It’s not as bad since you can always use a powerful programming language with a good type system that avoids type errors at the SQL level. You can build good abstractions in your programming language.

Lending or selling ebooks necessarily requires DRM. A large part of the community thinks having DRM is way worse than not being able to lend or sell.

Yes, the problem exists either way. Editions just exacerbate the problem.

Editions make the problem worse by requiring the version not only to support the underlying pragmas but also to understand the edition mapping.

Example: PRAGMA foo=1 is introduced in 2027. PRAGMA edition=2030 implies this foo pragma. Now you unnecessarily lock out three years worth of releases.

SQLite is slightly different from Rust in that it is a data container. It’s somewhat more common for people to move SQLite database files from one machine to another and then inspect using the command line tool. And it is often the case that the embedded SQLite version in your app is a newer version than whatever version /usr/bin/sqlite3 happens to be. Adding editions to your SQLite file will probably break this use case of using an older version to read a database written by a newer version because it does not know what has changed in a new edition.

Not a big deal though. Probably just need better ops to bundle the command-line utility that’s the same version as what’s used in your app.

Last year, the FDA had already said that if kratom is added to food, it is considered adulteration of food. It also cannot be a dietary supplement.

https://www.fda.gov/news-events/public-health-focus/fda-and-...

I’m not fully cognizant of the interaction between FDA and DEA, but I would’ve thought that following FDA’s announcement last year, kratom had already been outlawed.

Especially my cheap consumer electronics. Sometimes they will charge, sometimes they won't charge

You can fix that by buying USB-C to USB-C adapters with 5.1 kiloohm resistors.

It should have taken the manufacturer less than one cent to include the resistors, but as a consumer product they will unfortunately cost at least a dollar each.

Yes exactly. The author’s design decisions only make sense if this is supposed to be a toy language. On using pthreads rather than fibers:

I decided not to use one. I wanted something dead simple — an approach I could explain in a paragraph, using tools every C programmer already knows. The trade-off is that you lose some performance with fine-grained blocking, but in many real-world situations, pthreads work fine if you use a worker pool.

Sure. You can take a large production Go app and measure how many user space threads are launched; it’s decidedly a lot more than the typical number of threads if you were using pthreads.

And the author didn’t really justify why select isn’t implemented other than implementation difficulty.

They stopped caring much about Creative Cloud. They were focusing on Experience Cloud which is their euphemism for their advertisement network (products like Adobe Tags).

It actually used to be paid. I paid for Affinity Designer when it came out first, then Affinity Photo. I didn’t pay for the publishing software since I was too deep into TeX. But at that time they promised that they would never become subscription software like Adobe and that message was part of the reason I bought it. I liked and still like perpetual licenses.

When I was a novice in protobuf I felt tempted to inspect the generated code, but soon I learned that the documentation is good enough that I don’t need to read the generated code.

It’s very much Terrence Tao style. His style is having long sentences that could have been broken down into shorter sentences but he chose not to. It doesn’t really affect reading comprehension.

It’s a criminal charge. Have you seen a legal case for that? It’s always something like The People of California v. Someone. At least in theory, every citizen is an interested party when the prosecutor files a criminal case.

There are far too many corners of logic for everyone to know. Maybe someone has never dealt with data streams, or even forgets what a median is.

Bad interviewers expect candidates to know things. I don’t. It’s okay for a candidate to have never worked on data streams or to forget what a median is. I simply provide the definition and continue. I care about the quality and effectiveness of thinking. If the candidate can be given a definition and then immediately turn that into code, that already shows that they are good at logical reasoning. It’s basically the same kind of thinking required when there is an urgent request at a startup and an engineer is pulled in to come up with a solution quickly; all the business logic will be new and you want someone who can learn quickly, internalize quickly, and produce results based on these learnings quickly. Therefore in my opinion asking these interview questions are actually a good indicator of how they will perform in a hectic startup environment.

Humans will do this as well, especially inexperienced junior SWEs. Adding a new boolean parameter and some if statements here and there. After a while a seemingly simple function takes four boolean parameters that each control a little bit of what the function does.

The benefit is that a human who is a junior might need at least a few weeks to months of guidance to have a good taste of when to duplicate and when to DRY. An LLM likely already has good judgment, and your prompt merely needs to be activate this judgment.