Hacker News Reader

m_j_gon Time to Move On – The Reason Relationships End

to the point, that it is reasonable to commit altogether to the choice.

m_j_gon Time to Move On – The Reason Relationships End

This made me think of the secretary problem.

Early in life it makes sense to move on more easily, not because we value people or partners less, but because we’re still figuring out ourselves and how the world works. There’s just more uncertainty.

Later, when we know more about who we are and what fits, it’s natural to switch less.

https://en.wikipedia.org/wiki/Secretary_problem

m_j_gon Man wearing metallic necklace dies after being sucked into MRI machine

In Poland you can get one without doctors referal (for CT you need one because of ionizing radiation exposure), it cost between 100-200$ in normal, reputable hospital (not one like from the street view).

m_j_gon Homotopy Equivalences

vaguely related : synthetic homotopies visualisation tool - https://github.com/marcinjangrzybowski/cubeViz2

m_j_gon How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

Did you played with cubical flavor of Agda? here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2 :)

m_j_gon Ask HN: What's is your go to toolset for simple front end development?

secound, espeicaly together with elm street for generating code from Haskell

m_j_gon Timeline of “foundational” advances in homotopy theory?

From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)

m_j_gon Dbcritic: Constructively criticizing your Postgres schema (using Idris)

It is nice to see practical application of dependently typed language!

m_j_gon Where are we going from here? Software engineering needs formal methods

Contrary, formal methods could (in theory!!) give as way to assess correctness of software regardless of programmer qualifications.

m_j_gon Veritasium: A Physics Prof Bet Me $10k I'm Wrong

previous video that led to wager : https://news.ycombinator.com/item?id=27330412

m_j_gon Homotopy Type Theory

cubical Agda : https://github.com/agda/cubical is also worth mentioning int this context

m_j_gon Ask HN: Books for Effective Communication

Messages: The Communication Skills Book Di Matthew McKay, Martha Davis, Patrick Fanning

Basics, without any controversial ideas. This book helped me a lot.

m_j_gon Why we chose Elm for Humio’s web UI

I am very happy with Elm on frontend. When working with Haskell I tend to generate most of frontend types for Elm directly from haskell with elm-street (https://hackage.haskell.org/package/elm-street)

The downside of Elm simplicity in comparison to haskell is inability to express even simplest typeclases like Ord, or very useful constructions like Lenses.

m_j_gon Ask HN: What under-the-radar technology are you excited about?

Dependent types and homotopy type theory for general purpose programming. I am definitely excited about it, but not really sure if those hopes will ever materialize as some useful (even in the limited scope) technology.

m_j_gon Ask HN: What's your absolute favorite tech stack, after having tried others?

tried multiple stacks for last 12 years, for past two years I am enamored with Haskell + Elm

m_j_gon Ask HN: Solo developer, what's your recipe to start working?

Some time ago i discovered, that when I am unable to write code, I am still able to engage in less demanding but still very beneficial activity for my project:

Pair programming with less experienced members of the team. It was very important for me, because previously, when i had "bad day" i was ending with completely wasted day. Now, even when i am not able to do work myself i am still able to boost significantly someones output.

For solo projects, watching advanced tutorials, or conference talks about technology beneficial for current project gives me sense of progress during days when i am unable to code.

m_j_gon I can only think that modern front end development has failed

I think that this branch of engineering is still in its infancy (like electrical engineering int the times of edison). I am courius how front end development will look when dust will settle, maybe in 50 years?

Maybe todays, heated disucions will be setted for good? Or something new, better will be invented?

m_j_gon How do you stay grounded when writing software no one wants?

If you want to keep this job, but looking for some motivation: Maybe try to focus on developing good (expert level) craftmanship?

If overall quality of project is poor, it maybe even be possible to find some narrow aspect which is possible to polish. Expertise gained that way may be used later, when you finally start working on something meaningful in the future.

m_j_gon Ask HN: What (side-)project are you working on?

https://raw.githack.com/marcinjangrzybowski/cubeViz/master/m...

Visual editor for cubical-agda code, currently I am rewriting it in haskell and integrating with emacs. New version will allow to edit code in 3 and 4 dimensions :)

m_j_gon 5 years of leetcode with no progress. I'm giving up

Because of the structure of labor market, for highly competitive jobs luck is also very important: https://www.youtube.com/watch?v=3LopI4YeC4I

It does not meant that merit do not play role, simply there is so many highly skilled, and good candidates, that only small percent of them will get the dream job.

m_j_gon A curated list of FOSS tools to improve the Hacker News experience

I am fan of some niche technologies, I would love the functionality of “white list”, which would show “new stories” on the main page if new story contains some specific keyword from predefined set (ideally not only in title but also in content of linked page)

m_j_gon Vim Clutch – A hardware pedal for improved text editing (2012)

Since I've got a "emacs pinky", I started to using this, and really like it:

https://www.amazon.com/iKKEGOL-Triple-Keyboard-Control-Hospi...

m_j_gon Ask HN: What is your current side-project?

https://raw.githack.com/marcinjangrzybowski/cubeViz/master/m...'

Visual editor for cubical-agda code, currently I am rewriting it in haskell and integrating with emacs. New version will allow to edit code in 3 and 4 dimensions :)

m_j_gon Procrastination is flight, deadline is fight, freeze is staring at the screen

I have very similar story, it was mind-blowing to me how methylphenidate pharmacotherapy helped me not only with procrastination but also gave me capacity to work on anxiety/depression and interpersonal issues.

In no way I want to advertise mph as a silver bullet for such problems, but at least for some people it works like a charm.

m_j_gon Haskell's Children

Did you tried to incorporate cubical agda into some real world development? For me it is cool to let internal machinery handle isomorphism between different types, but cubical agda library is still much smaller than std agda library ;/

m_j_gon Topology from the Perspective of Category Theory

more homotopy than topology, but still may be interesitng to you:

https://staff.math.su.se/anders.mortberg/papers/cubicalsynth...

m_j_gon Black silicon photodetector breaks the 100% efficiency limit

"The external quantum efficiency of a device is 100% when one incoming photon generates one electron to the external circuit. 130% efficiency means that one incoming photon generates approximately 1.3 electrons."

m_j_gon Seemingly impossible functional programs (2007)

You may be interested in his brand new course on HoTT in Agda

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...

m_j_gon Ask HN: What kind of math do you study in your free time?

homotopy type theory!

m_j_gon Ask HN: How to rediscover the joy of programming?

There is nothing special about them. I am talking about simple formalisation, there is already some code about finite types in cubical-agda library, so it would be good place to start.

I think that usefull definitions and properties can be formalised in ~100h.

Matroids are known to be good example of cryptomorphic structures, so cubical agda can be used so that those cryptohmorphism can work "under the hood". I know how to do this, but I am currently working on something different. If You are interested pm me.