boxfire

Joined 11 years ago

Karma

376

Submissions

129

Member since

Jul 2

she/her Opinions my own

View on Hacker News

Recent submissions

Comment · 17 days ago

> if you were deploying code to the mars rover, and your colleague asked to do a code review before you pushed go, would you be offended?

Having done so, from both the asking and being asked, yes I was offended. And glad I was asked after actually doing it. And learned to be insistent in asking. We all have hesitation but we should realize that “expertise” is a relative illusion and peer review is the only standard of progress we have ever demonstrated to be (eventually) fool proof. There are no people I trust in any field to be right for the sake of their name or accomplishments. Society needs that feeling to be stymied and eventually eliminated.

Comment · 3 months ago

This is not bidirectional. The Davis-Putnam-Robinson-Matiyasevich theorem shows we can make a Diophantine equation that acts as a universal Turing machine, but there’s Diophantine equations that cannot be solved by Turing machines:

https://www.nlp-kyle.com/post/number_computability/

The smallest known Diophantine equation that cannot be solved by any Turing machine last I checked had ~8000 states as a Turing machine. This Turing machine cannot be decided to halt, and if it does halt in finite time then an (outer) Turing machine could execute it to predict that, so this lives beyond decidability:

https://scottaaronson.blog/?p=2725

I find it annoying that the response to this from the Chaitain perspective is to throw your hands in the air and say not all of math is predictable and let “equivalent to halting decidability” be the death of effort. There’s a richer field of ‘hypercomputation’ sitting beyond the pale, and I believe it will be topological applications that untwist this knot [pun intended]. I’m excited for the post Turing world but i dare say I won’t live to see it.

Comment · 4 months ago

It actually took only 9 months to work around, and the new method is actually quite effective. After fixing some early bugs it’s as effective as the original drill technique.

Comment · 4 months ago

Mars 2020 has a microphone. You can probably find audio out there but here’s some:

https://science.nasa.gov/mission/mars-2020-perseverance/soun...

Comment · 6 months ago

So yeah topological sorting is one element, but that global stack is a data race! You need to test set inclusion AND insert into it in an ordered way. Global mutex is gross. To do so lock-free could maybe be done with a lock free concurrent priority queue with a pair of monatomic generation counters for the priorities processed then next, then some memo of updates so that the conflicting re-update is invalidated by violation the generation constraint. I see no less than 3 CAS, so updates across a highly contentious system get fairly hairy. But still, a naive approach is good enough for the 99% so let there be glitches!

Comment · 7 months ago

Very cool! Just wanna point out that Mirror + Rotate is really just 3 different mirrors. Of course it may be more interesting to try to characterize the visual domains in terms of those 3 mirrors rather than trying to do so obfuscated between mirror and rotate.

Comment · 8 months ago

I am a huge fan of the work towards putting this in kanren as λKanren:

https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e8619...

A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality.

To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general.

So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference?

And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared?