Thomas Burdick @tfb@functional.cafe

And if I make up for last week's jig with the obscene title, by proposing an 8 minute long song lamenting a young man unjustly condemned to death in Derry?

I mean, it has a happy end! You can't ask for much more than that for music from Ulster.

#Irish #Trad #Ulster

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”

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 😂

#Trad

The bug is between 3.B.iii.d and 3.B.iii.e. Oh, printf debugging.

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...

https://sympa.inria.fr/sympa/arc/coq-club/2019-03/msg00081.html

#Coq

I should also really look into extracting #Coq to #Go. That certainly won't solve the same set of problems I want an interpreter for, but should nicely complement it, if I can do it efficiently.

And given how magic the Go GC is, maybe even if it's consy and only half-efficient

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.

Irish stew and soda bread. Salmon and salad. Jigs and reels. Planxties and walzes. Porter and whisky.

No Justice in Derry, but still ... Happy St. Patrick's Day!

#NowPlaying
Tonight we played "Merrily Kissed the Quaker" https://youtu.be/qbzOfHe5C1k

Fun, traditional, and oh man is it a blast to play on the tin whistle. I can't quite manage the high bits on the pipes. Will be working on that this week 😁

#Trad

Dragging a set of Uilleann pipes through rush hour traffic in the métro is no fun. But I made it, and now I'm about to have a fun evening.

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.

#Important #Topics in #microelectronics #CAD ( #CAO ) for possiblity a single practitioner.

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.