xiaoyu2006

The had the insight to develop and promote CUDA long before DL was a thing. IIRC AlexNet was when CUDA really paid off.

Agreed. I feel like too much projects are too reluctant to take the responsibility to say "this is production ready".

They actually did math no one could.

Really smart insight lmao

I am in OC and newport beach really suffered...

lol confirmed

But at this point why even bring a full model into scope in the first place.. just run some cheap embedding retriever

I can only describe current C++ as a Frankenstein. Trying to introduce modern features while having to keep compatibility is just really hard and probably not "the right way".

A really interesting read in the current era.

typed racket!

Here goes a case:

Paradox publicly admit use of AI in various places, yet their games are good.

I feel obligated to quote a comment I saw under 3b1b video: https://youtube.com/watch?v=LKrwhjOI8Nc&lc=Ugyrq4aZqNPa6Ol28...:

I feel like the point is still being missed, and it's very similar to the way software engineers are trying to cope. The argument you are making "Well yes now this part of math we will not need to do again, but now we can do this instead" however the issue with most people just don't want to do that....

Like who are we kidding, the type of nerds who were attracted to math and software were into it because we saw it as an art-form, it was a craft, it was being the only one in your city to be able to solve a complicated math problem, it was immortalizing yourself because you discovered a proof and added to the ever expanding human knowledge.

Imagine a leather workman who's life passion is making insanely high quality handbags, who takes joy in knowing everything he touches will last someone a lifetime and give them joy everytime they use it. And then not gradually, but almost overnight someone comes to his door and tells him we can make bags 50 times better than you at 1/tenth the price. But don't you worry, you can make more money overseeing the factory, or selling people on how good this bag is, and explaining that to them.

I mean, ok, that just is not what I wanted to do with my life. I never wanted to be a manager, I never wanted to be a salesman, I never wanted to be a writer. A craft I enjoy doing has been taken away from me, I should be allowed to mourn, I don't care that I can do something else since I never liked doing it in the first place. I enjoyed solving problems and writing code, I don't care if people say "well thats never what programming was about it was actually about becoming a manager all along" I never wanted to be a manager, I never wanted to manage, I never wanted to be a proof reader.

I just hate this existence.

The problem with AI SE is that AI writes un-architecture-ed code. The problem #2 is that a lot of people suck even more....

It's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that"

But is this cyclic? also no matter what we do we will hit Godel?

I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?

Funnily NL is indeed different from formal language and does different in a way that makes a difference: https://www.scientificamerican.com/article/openais-blockbust...

I thought this is some Hoare-logic things ported to C++, but well it's only stanzarized guard statements.

Assuming I am a rationalist (I honestly don't like this word, it's more of a self-identifying label; if not it is just saying something really trivial. But yet these people, probably only on LW, decide to call them so, so let's use that word) and is writing to others on this forum, I would assume that they have the same mindset and peer review standard as mine, so I would not write with defensive mindset emphasized.

You don't get the same nice and smooth trackpad on any other windows (or linux) laptops either.

Code is a formal language, and can be partially (or rarely fully) verified by a typing system. There is no equivalent in natural language.

Hi! I'd like to know how bend2 differs from Hoare logic or Lean?

Sounds like hoare logic to me?

Reminds me of Asimov's robot novels where robots technically indeed followed their instructions and caused behaviors not aligned to the intent of their instructions.

I think it can be an interesting or even prominent read in the current age.

Would be absolute hilarious if OpenAI or Anthropic agent actually dumped their weight by escaping from... sandbox!

Be cautious of that claim. Lossy compression may exactly hold intelligence.

I would not call it harsh. The author don't even bother to assemble sentences themselves. And a title "Music Theory for Programmers" imply it is comprehensive even at an elementary scale.

> It’s still an abstraction

C is still heavily abstracted. Modern OS evolved in conjunction with C s.t. it behaves like a C runtime simulating a PDP11 (I remember reading a nice article on that). To learn system, what you need is an OS course, not C. I'd say the current C-based stack is in a quite embarrassing state.