As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers.
I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.
Is there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.
It’s not about elitism. It’s that there are so many confounding factors that even a well-informed approach makes such a study comtain very little of value
Comments like yours expose a particularly distasteful amount of hubris.
You don’t like it you don’t have to read the blog article. I assure you are not the intended audience. For the rest of us it provided valuable insight.
Ignoring latency for a second, one of the tricks for boosting quality is to utilize consensus. One probability does not need to call the lesser model 30x as much to achieve these gains sorta of gains. Moreover you have to take the purported gains with a grain of salt. The models are probably trained on the evaluation sets they are benchmarked against.
Just an anecdote but I was with my young child in GG park not too long ago and perhaps 50 meters from the artierial road encountered a homeless guy brandishing an axe. This in in a spot that routinely fields families.
I’d like to say, “Is this not obvious?” but I’m not sure I fully appreciated what follows until I had a sufficient level of exposure to abstract mathematics. A core element of problem solving is reduction, be it to logically equivalent formulations or to more atomic components that can be reasoned about together.
I encounter some bogus undocumented password constraints probably half the time I create an account. Usually it is a maximal length requirement that is not mentioned in the error message.
I'm not. The only time I've seen a maximum length password was like 10 years ago on Dell's IDRAC I think? I just don't think the complaints being thrown out here are good arguments.
i just had it happen day before yesterday to create an account for a service to do a background check for a new job. it rejected my password without saying why and i could only get past it by shortening it to 15 characters.
and then the deeper question is, why do i need to create an account for this?
Not defending the max length, that's stupid and probably some old AS400 thing that got built into the system, but the account is for auditing obviously.
The portability is almost equivalent to the form factor itself, in many cases.
To the point you’re responding to, I can actually think of numerous scenarios where my phone is the preferred device to “send texts.” This activity is not simply the single dimension of “length.”
I think kurthr made a great point in a parallel comment – in what scenario would you switch to your phone to answer a message if you are already sat in front of your computer (assuming the relevant apps are on both devices)?
A generic homomorphism does not induce any isomorphism to a subset of B that I can think of unless it is already injective. The isomorphism you’re after is rather from the quotient structure of A mod the kernel to the image.
I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.