lacker

7 ms·

61.
by lacker 11mo ago
That's a good point, for example in Eigen you can do Eigen::Matrix<float, 10, 5> I just really want it in Python because that's where I do most of my matrix manipulation nowadays. I guess you also would really like it to h
62.
by lacker 11mo ago
Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that. The Curry-Howard correspondence, using dependent type system to ha
63.
by lacker 11mo ago
The only thing I dreaded more was trying to run other people's C++ projects.
64.
by lacker 11mo ago
It's like the negativity whenever a post talks about hiring or firing. A lot of people are afraid that they are going to lose their jobs to AI.
65.
by lacker 1y ago
For anyone that's interested in formalizing mathematics but wished there was an easier way to do it, I've been working on a different sort of theorem prover recently. https://acornprover.org The idea is that there&#x27
66.
by lacker 1y ago
I whitelisted github.com, api.github.com, *.github.com, and it still doesn't seem to work. I suspect they did something specifically for github to prevent the agent from doing dangerous things with your credentials? But I could be wron
67.
by lacker 1y ago
The sandbox idea seems nice, it's just a question of how annoying it is in practice. For example the "Claude Code on the web" sandbox appears to prevent you from loading ` https://api.github.com/repos/...&
68.
by lacker 1y ago
They're renaming Coq, too, for the obvious reason. Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not.
69.
by lacker 1y ago
Personally, I'm not religious. But 20% of Americans believe that the Bible is the literal word of God. Is it really so crazy for one venture capitalist to believe that the Antichrist is real? Part of the freedom of religion is acceptin
70.
by lacker 1y ago
It is not a sin to hire people when you aren't 100% confident your business is going to succeed. That's just how startups work. Some people are not in a position in their life to take any risk of losing their job, and that's
71.
by lacker 1y ago
> Sam is spinning the world on his finger tip with these deals he's crafting. That was my reaction too, this sort of weird deal seems very Sam Altman style. Like Elon Musk - ironically, the archenemies are very stylistically similar
72.
by lacker 1y ago
Type hints are much easier to use nowadays than they were a few years ago, because the agentic tools like Claude Code are very good at converting an existing codebase to using type hints.
73.
by lacker 1y ago
We DID build good transit. It takes 15 minutes to get from the MacArthur BART to downtown San Francisco! But the walkable area around that station is full of single-family housing. It's a huge waste building all of this incredible publ
74.
by lacker 1y ago
A big question is whether these areas actually turn into denser housing, or whether something else in the process manages to bog it down. Plenty of housing bills have seemed like a big deal when you looked at the area they impacted, but in
75.
by lacker 1y ago
Of course a crime-fighting company "sells to police forces and corporations". Who else would you sell crime-fighting tools to? Flock reminds me of Replit: they both predate the modern era of AI, and in some sense they were lucky t
76.
by lacker 1y ago
I'm confused, I feel like the two of you are expressing opposite opinions. The comment you are responding to prefers green threads to be managed like goroutines, where the code looks synchronous, but really it's cooperative multit
77.
by lacker 1y ago
I think LLMs are different because they are such a powerful developer technology. The most powerful I have seen in 25 years. Some engineers went from useful to useless almost overnight. Someone who is stubbornly stuck in their ways and refu
78.
by lacker 1y ago
It sounds better than the northern California system where occasionally PG&E will cut off the power of random neighborhoods because the grid is overloaded.
79.
by lacker 1y ago
This claim from the article is too extreme: "It is safe to say that prior to 1610 not a single significant scientific argument had turned on a question of fact." Just in astronomy alone, in the previous century Tycho Brahe was deb
80.
by lacker 1y ago
In my experience the FAANG companies don't really abuse their H-1Bs. At Google or Meta the H-1Bs really are just smart people who participate as full and equal peers. And the FAANGs employ plenty of American citizens, they hire all the
81.
by lacker 1y ago
By the time they are hoping to finish in 2029, I bet LLMs are capable of translating the proof from Lean into the alternate theorem proving language of your choice with only a small amount of human assistance. If this does end up being the
82.
by lacker 1y ago
Draw 99 circles in a row, then draw a separate polygon around each one with only a teeny amount of excess area, then connect those polygons with teeny little connectors to make it a single polygon. When I say "teeny", you can make
83.
by lacker 1y ago
Typically formalization is actually harder than solving a problem. You almost always solve before formalizing. And it can be surprisingly hard to formalize problems that are easy to solve. For example, is there a polygon of area 100 that yo
84.
by lacker 1y ago
Will the other models really catch up, though? To me it seems like Anthropic's lead in programming has increased over the past year. Isn't it possible that over time, some models just become fundamentally better at some things tha
85.
by lacker 1y ago
Yes, unfortunately, they have changed their permissions structure a few times, and each time I have had to go back in and re-configure it so that the ads don't show up. It's quite annoying, they seem to be doing everything they ca
86.
by lacker 1y ago
I think there's a mistake in the explanation for "bathroom_stall". When describing the guard in this expression: if (i+=1) != (i+=1) The post says, "The if statement is always going to be false because the right e
87.
by lacker 1y ago
It's not impossible, that's the whole point of a theorem prover. You write a computation, but you don't actually have to run the computation. Simply typechecking the computation is enough to prove that its result is correct
88.
by lacker 1y ago
In Lean you don't actually have to run this for every n to verify that the algorithm is correct for every n. Correctness is proved at type-checking time, without actually running the algorithm. That's something that you can't
89.
by lacker 1y ago
It took me a few tries to get through Ulysses, but I enjoyed it when I finally figured it out. What helped for me is first reading A Portrait of the Artist as a Young Man, which is kind of like an easier version of the same style that intro
90.
by lacker 1y ago
I already do understand set theory and the construction of the real numbers. There are plenty of great books on that, or really nowadays you can simply ask ChatGPT. I am interested in learning about how Cantor, Weierstrass, the ancient Gr

More ›