runeblaze

beats me. I spent so much time learning what a fundamental group is and I still cannot tell ppl what a fundamental group is convincingly.

I can’t even make stuff with fundamental groups.

Ummm guys when we talk about memory access in theory can we just be rigorous and talk about the computational model?

The real RAM model “in theory” tells me that memory access is O(1). Of course real RAM is a spherical cow but like we could use a bit more rigor

Of course it seems to be the same person to have done minecraft inside minecraft using redstone :)). peak!! done it again

Yea experience is very useful (it is very hard to exert influence without power and be the tech lead of a team unless you have some corporate experience) but at some point one needs to realize that if someone was writing Haskell at the age of 12 and they got decent scores at USACO they would make quite a decent engineer...

Python types - all the onus of static types, with none of the power of calculus of constructions. /s

sure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple

> How proofs work is really simple

idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).

Also how proofs work is far from simple.

idgi tho. The average working mathematician seldomly thinks about proof theory or how proofs "work". Proof theory if must be put in a single box it is an logician's art, and at that point it is niche enough in both CS and maths that it becomes meaningless to say mathematicians know more about it. Logicians are better at thinking about proofs than either maths people or CS people.

I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.

I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.

ZF(w or w/o C)/type theory/other foundations of maths are "equally" right? My argument is that even if we are trying to build PAs from scratch, type theory provides tangible benefits to the working mathematician because we can just borrow CS research in many stuffs like proof checking and synthesis.

Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..

I mean sure we can do ZFC or ZF as the foundation, and I am sure with enough effort we can make metamath or some modern derivative great again. At some point though I like having years of type-directed program synthesis research helping me write proofs; I like type-checking research helping me check my proofs, and I like my proof assistants to work well for verified program extraction if I also happen to write code because the mathematics academic job market is quite shit for your average pure maths PhD, and if I were to do logic then it might be even shittier.

Admittedly the above (except program extraction I suppose) can all be achieved with ZFC + a layer of type theory on top, and again that's a reasonable thing to do, but I hope this makes a strong enough case for the type theoretical foundation.

That story reads like what happens when the average senior engineer tries to do a hardish usaco problem; turns out algorithm engineering is different from your average enterprise engineering; turns out there are people in both camps

The coin problem is like the intro to it. Try some of the codeforces one :skull:

> Today many online poker sites use the Fisher–Yates algorithm, also called the Knuth shuffle (which sounds delightfully like a dance). It’s easy to implement and delivers satisfactory results.

Assuming CSPRNG and fisher yates, why is it only "satisfactory"...? What's better...?

Technically Koka checks your box. You also get algebraic effects in the same bundle

For these unfortunately you should dump most of the guide/docs into its context

Yep also people with differences in sexual development ("intersex", sometimes) are also overrepresented in trans people for obvious reasons. It is like extremely murky

I literally don't even write proofs in my head. Every time I write algo I just ask Cursor for a Lean/Rocq proof of correctness. No tests. No test coverage. The sheer power of type theory

Same here. Turns out writing too much code for RPG Maker XP when young ruins one’s perception of Ruby forever

I mean tbh industry research labs pump out a lot of good research due to them being intern projects (as in you have an army of passionate interns)

I mean we don't really talk about the accuracy of generative models. It is more of a discriminative model thing.

But besides this, the current gen of models still, like, hallucinates more than many would like

It is weird to be honest. I first learned Coq and then started taking upper level maths classes. My group theory proofs were panned by my TAs as overly verbose, very precise, and I was specializing on H_1 and H_2s everywhere and having IHns flying around like crazy because I could not fathom how one proves things without formally connecting things up.

Then my profs told me I was not “wrong”, but proofs or expositions are to most mathematicians not programs (ha! How did I not know. You teach me natural deduction and expect me not to program?), more like convincing arguments/prose. At some point one abstracts.

there kind of is, but also note we are talking about the exceptional talent here. I don’t think Meta is mass poaching the pure engineer types at OpenAI either

It has obvious pros, but since you asked about the cons —- anonymity brings the worst out of people; TC chasing leads to a reductionist view of people’s values and skills.

For example unlike HN you don’t often do technical discussions on blind, by design. So it is a “meta”-level strategy discussion of the job, then it skews politics, gossips, stock price etc..

This is compounded by it being social media, where negativity can be amplified 5-10x.

I am sure as ideation devices these can work fine. I treat this more like basic infra. I would absolutely love the future where most phones have some small LLM built in, kind of like a base layer of infra

Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard

    Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x.

Then immediately I dropped that class. Turns out I like real analysis much more

It is humor. I don't watch south park to be persuaded for example.

My opinion is that at least (safe, not spiro) anti-androgens should be able to be bought OTC. If some people want to place blockers on themselves they should be allowed to. I mean if you don't allow them to they DIY

Yeah like I very much respect their work, and there is some genuine beauty in having this policy such as "have access to > 100k USD in the last 365 days, this tier is for you" or the fact that they seem dedicated to also support small indie creators. However this does differentiate them from true FOSS solutions.

Note that small game devs have many types, and I imagine these "boutique" pricing solutions can work for many.

Yeah probably if they were writing a paper, encoding `.raw` files would have served them better (for being more convincing)

1. You are right 2. My guess: even among people who code professionally (e.g. data scientists), the same applies