Shahid coming with some serious wisdom here: https://twitter.com/shahidkamal/status/1109194985285533699
4. Once you can mimic well, start to improvise. Just like when you’re learning to speak, sometimes you’ll sound foolish. And one day, if you refuse to let sounding foolish stop you from experimenting for long enough, you’ll be Mozart, or better still, Dijkstra.
[A]s Wilde wrote, “we are all in the gutter, but some of us are looking at the stars”
Breaking news in the algorithmic/arithmetic world!
Integer multiplication in time O(n · log n). 
It means you can multiply two n-bits integer using roughly n log n operations. It's a *very* important problem because a lot of mathematical software rely on efficient integer multiplication.
It breaks the last best known algorithm  (Schönhage–Strassen), that was in O(n · log n · log log n)
Going to propose playing "An Phis Fliuch" tonight: https://www.youtube.com/watch?v=Hzi7OhSzysw
"I wonder what that means in English," I think to myself. Also, people appreciate English names rather than Irish ones. "Oh my, that's obscene."
I guess that's why the tune name is always given in Irish 😂
I guess moral of this whole story is to handle the user input as hazardous waste, with ridiculous attention to all the details.
Yet there is surprisingly little ready-to-use building blocks for doing that in actual software; rather converse, the developers tend to neglect it spectacularly.
I do not enjoy this topic very much, TBH. Especially digging up the proprietary s/w, which contains way more of these opportunities.
But it seems like not many developers realize how much real the concern is.
Well this is interesting:
To have a good notion of equality ... it's better to define it ... so that proofs of the proposition "-1 < x /\ x < max" are unique.
Proofs of a negation ~P are functions, so you cannot show that there is only one proof of ~P, even if there is only one proof of P. Unless you assume function extensionality, of course.
So, "-1 < x", which expands to "Z.compare (-1) x = Lt", has unique proofs, but "0 <= x" or "x >= 0" does not...
Current frustration with #Go: if this is supposed to be a low-level language, why isn't there a computed goto of some sort (switch with densly packed integers, for example). If this is supposed to have high-level aspirations, why can't we get tail-call merging? Even for local functions?
It's so close to a good language in the genre it's aiming for, it's infuriating to have nothing to build an efficient Interpreter atop.
This morose, nostalgic though was provoked by https://mathstodon.xyz/@amiloradovsky/101747044929598812/
I wonder if some of the #HoTT folks aren't trying to sneak God back in to logic. But if so, they'll be confined to a local area.
What I can say, what I deeply appreciated in his work, even when he was facing death and failing utterly. I appreciate that he was able to wall off God and not let him into his work. "The Structure of Evolutionary Theory" is a masterwork, and bears little to no trace of Gould's failure to face mortality.
Compare this to Dawkins, who, for all his obnoxious petty-bourgeois atheism, cannot stop sneaking God and class society into his science.
I'm of the generation that had our hearts broken by Stephen Jay Gould. I devoured "Ontology and Phylogeny", "The Mismeasure of Man", his essays, his academic articles, his book reviews. The man wrote with a deep understanding that biology hadn't seen since Darwin. But he stood even higher; he'd read Engles, Hegel, Lenin, and could draw on that in his science.
I was 21 or 22 when I read "Nonoverlapping Magisteria", and I cried real tears. I'm still not over the heartbreak 20 years later.
math meta Show more
"In any case, the skeptical reader should keep in mind that the standard of rigor in formalized proofs is at least a great deal higher than the generally accepted level of rigor in traditional written mathematics"* — Yup.
I've often heard that "mechanization" of mathematics is not a "game changer", that it adds nothing principally new etc. etc. — Of course it doesn't, nobody is claiming it does. Still nice to have it though.
While I'm over-using the word "intuition": are you like me, trying to solve 2D geometry problems, but have a poor intuition for vectors? Try my technique: go ahead with solving the problem however you conceive of it ... triangles, shape transformations, however. Keep an eye out for math that looks suspiciously like vector math. When you spot it, STOP and find the vectors hidden in what you're doing. They're often the easier way if doing things once you find them.
Lisper/Schemer, CAD software developer, dependent types enthousiast.
Programming should be more accessible.
English, Français, Deutsch. He/him. France
functional.cafe is an instance for people interested in functional programming and languages.