almostgotcaught

> Your obsession with finance/marketing is exactly what I expect to see on HN.

homie i work on AI infra at one of these companies that you're so casually citing in all of your marketing content here. you're not simply wrong on the things you claim - you're not even wrong. you literally don't know what you're talking about because you're citing external facing docs/code/whatever.

> attempting to get into technical discussion, and promptly backing out of it having not made a single technical argument in the process

there's no technical discussion to be had with someone that cites other people's work as proof for their own claims.

> NVIDIA has lost, just that GPU's have lost

i hope you realize how silly you sound when

1. NVDA's market cap is 70% more than GOOG's

2. there is literally not a single other viable competitor to GPGPU amongst the 30 or so "accelerator" companies that all swear their thing will definitely be the one, even with many of them approaching 10 years in the market by now (cerebras, samba nova, groq, dmatrix, blah blah blah).

Is your answer to "where can I buy a TPU" that you can't buy a GPU either? That's a new one.

First of all I don't understand how that's an answer. Second of all it's laughably wrong - I can name 5 firms (outside of FAANG) off the top of my head with >1k Blackwell devices and they're making very good money (have you ever heard of quantfi....). Third of all, how is TPU going to conquer absolutely anything when (as you admit) you couldn't run one even if you could buy one?

> Unfortunately, GPU's are old news now

...

> the recent Versal chips allow for AI compute-in-network capabilities that puts NVIDIA Bluefield's supposed programmability to shame

I'm always just like... who are you people. Like what is the profile of a person that just goes around proclaiming wild things as if they're completely established. And I see this kind of comment on hn very frequently. Like you either work for Tenstorrent or you're an influencer or a zdnet presenter or just ... because none of this even remotely true.

Reminds me of

"My father would womanize; he would drink. He would make outrageous claims like he invented the question mark. Sometimes, he would accuse chestnuts of being lazy."

> I think it's very naive to assume that GPU's will continue to dominate the AI landscape

I'm just curious - how much of your portfolio is AMD and how much is NVDA and how much is GOOG?

> what is likely to happen on the various problems

Pure math just doesn't work like that. Literally no one has any idea when XYZ problem will be proven - there's no way to know! It's not like building a stadium or a road or even a company , where you can see or anticipate the coming of a proof before it arrives. It could happen tomorrow or it could happen never. For example, of Hilbert's original 23 problems posed in 1900, three are still open.

What a weird comment/expectation. He's an academic mathematician not an influencer. What exactly do you expect him to predict - whether the Riemann hypothesis will be proven?

so?

Almost every compiler is a multipass compiler.

> The second offer does not have to be real

Lol people explicitly directly ask to see offer letters. Bluffing like this is a great way to actually have the negotiations end prematurely because you're found to be operating in bad faith.

> Functions taking more than 3 arguments. Currently PyTypeBuilder.add_function() and related function bindings only support Mojo functions that take up to 3 PythonObject arguments: fn(PythonObject, PythonObject, PythonObject).

Lol wut. For the life of me I cannot fathom what design decision in their cconv/ABI leads to this.

> In essence, caches allow hardware to be flexible and adapt to a wide range of applications. This is a large reason why GPUs are very flexible hardware (note: compared to TPUs).

this is correct but mis-stated - it's not the caches themselves that cost energy but MMUs that automatically load/fetch/store to cache on "page faults". TPUs don't have MMUs and furthermore are a push architecture (as opposed to pull).

they have lots of money and they use that money to pay software engineers (their employees...) to write quality software.

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect.

This is irrelevant.

> You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the recursive maxDollars_spec.

Yes my original comment said exactly this.

The rest is irrelevant.

Reread my original comment again - or any of my follow-up comments - I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

You think the company that supplies every hyperscalers is market leader because of the hobbyist segment? Lol

> Given that both `maxDollars n` and `maxDollars_spec n` are defined to be natural numbers, I'm not sure why Richardson's theorem is supposed to be relevant

Did you know that the naturals are a subset of the reals? If Richardson's doesn't convince you there's also

https://en.m.wikipedia.org/wiki/Rice%27s_theorem

> Examples

> Is P equivalent to a given program Q?

Irrespective of where you're convinced it's 100% true that equality of two functions is undecidable in general.

citation please

a distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.

> These ppl are very loud online, but they don't make decisions for hyperscalers which are biggest spenders on AI chips.

this guy gets it - absolutely no one cares about the hobby market because it's absolutely not how software development is done (nor is it how software is paid for).

it's all just called gcn now

https://llvm.org/docs/AMDGPUUsage.html#id38

> you can write an inductive proof that x^2 * (x^2 - 1) is divisible by 4 for all x

my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation.

the obvious indicator is that no property of any numbers is checked here - just that one function agrees with another:

  theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n

this is the part that's undecidable (i should've said that instead of "impossible")

https://en.wikipedia.org/wiki/Richardson%27s_theorem

it's explicitly stated in the article:

> For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof

if you thought harder about it you'd realize what you're suggesting is impossible

it's explicitly stated in the article:

> For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof

if you thought harder about it you'd realize what you're suggesting is impossible

i don't know what you're saying - here is the proof that is described in the article:

1. build a table tab[n]

2. check that for every i, tab[i] == maxDollars_spec[i]

if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.

This is proof by exhaustion: the "proof" just computes the entire memo table for any n and compares the values in the table with the corresponding return from recursive definition. You could write this same proof in absolutely any language that supports recursion (or not, if you transform to the bottom-up formulation).

> by claiming that other comments are so egregious that the guidelines shouldn't apply to you.

no man i keep claiming the same thing over and over: that you have done nothing about any other comment in this thread except mine. i've literally said this same thing like 5 times. and what's happening is you keep reasserting some kind of lattitude to ignore them.

> I'm not going to be goaded or shamed into acting on comments on the basis that "it should be obvious". We can't operate a site like that.

you can't have your cake and eat it too: if my comments are obvious enough given a particular value system that you can scold and censure me, then there can be plenty of others that are just as obvious.

edit:

> rather than insisting that you are above the guidelines... take responsibility for your own conduct

please point out for me (by using links) where i didn't "take responsibility"? at multiple points i admitted to being sarcastic/flippant. how would you like me to further take responsibility? would you like me to apologize to those people? would you like me to delete my comment so that they continue fly under the radar? would you like me to commit hari-kari?

> You're expecting us to moderate a particular way about topics you have particular knowledge about and particularly strong feelings about. That's not something we can ever do, no matter the topic or the side. This is a perfect example of why it matters to optimise for substance over indignation.

This is such a weird false-dichotomy you're portraying. No one is expecting you to weigh in on arcane/abstruse things. This is about a current holiday in America that commemorates freeing of slaves ~150 years ago, not slavery in the Mycenaean civilization of 1100BCE.

You said you're not American - ok then maybe you should've stayed out of the thread entirely? But since you didn't, then you should realize it is your responsibility to educate yourself. Like just plain and simple: can you imagine a police officer policing a foreign people being unaware of their history/culture/etc?

Like can you imagine the same thread about mistreatment of aboriginals in AU - would you similarly blithely claim ignorance? Indifference?

> All we can do is respond to the bad stuff we see, which we can only do if people use the site's feedback mechanisms to alert us to things that need our intervention.

....

> Of those comments, one of them would be killed by now if you'd just used the site's functionality as intended and flagged it.

Am I taking crazy pills? I directly linked you to both comments, you concede one of them crossed a line, and yet this morning I wake up and they're both still live simply because I didn't hit a specific button?

And no I'm not gonna hit the button. Because my point isn't actually about political bias or whatever - it's that you people are weirdo hall monitors that tone police instead of actually encourage discourse (as I've said many times now in this thread, despite your claims that I'm complaining about bias).

[flagged]

I wasn't implying it's biased against me - that would be banal - I'm implying you don't actually care about healthy discourse but keeping up appearances because the only thing you're responding to is my purple language and not all the hate speech.

Edit: I'm rate limited

> you're not doing your part to help

... I responded to a comment and pointed out a revisionist take. Did you scold that person too or just me? Do you get it now?

Lol ban me I'll just make another account (and I know you guys think you have just the best fingerprinting tech but newsflash you do not :)