a thoughtful web.
Good ideas and conversation. No ads, no tracking.   Login or Take a Tour!
dyad's profile

x 3

following: 16
followed tags: 0
followed domains: 0
badges given: 0 of 1
hubskier for: 1406 days

AKA Devac.

recent comments, posts, and shares:
dyad  ·  1397 days ago  ·  link  ·    ·  parent  ·  post: Hubski, what are some of your favorite words, in English or any language?

English: huggermugger. It's so confusing (hugger + mugger = clandestine work) that you cannot just pass by it without rising an eyebrow.

Polish: dykteryjka (short, funny story) and imponderabilia (things which are incalculable, but affect other things, like luck, state of mind, or similar).

dyad  ·  1398 days ago  ·  link  ·    ·  parent  ·  post: Hubski, what are you working on?

Tip for future QM problems: write n subscripts in phi and normalization factor. It's sometimes easy to lose the explicit relationship, and it's one of those omissions that can waste a lot of your time when it's least convenient.

dyad  ·  1399 days ago  ·  link  ·    ·  parent  ·  post: Proving the relationship between the golden ratio and the Fibonnaci numbers in Coq

What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting.

Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P

dyad  ·  1403 days ago  ·  link  ·    ·  parent  ·  post: Pubski: July 31, 2019

Hi there. It's Devac, have some account recovery problems and made an alt. Sorry if I didn't respond.

The last two weeks were a tad hectic. I met lots of people, continue playing and anxiously await news on the PhD placement front.

My cardiologist is retiring, but she recommended me to one of her past residents, and he's been both understanding and accommodating.

mk - I used a non-gmail email for this account and messages from Hubski aren't filtered out. It's Wirtualna Polska (wp.pl - can't link), which probably won't help anyone, but it might be relevant for your diagnostics.

dyad  ·  1406 days ago  ·  link  ·    ·  parent  ·  post: Pubski: July 17, 2019

Thanks, I'll give it a look sometime. Not much of a fan of 'prequels', but this looks both interesting and promising.

Also, sorry for using an alt.