boxfire

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.

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.

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

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!

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.

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?

Fun to poke at, maybe just enough modern interest in logic programming to get there too…

It’s also funny because it’s a small, incomplete, incompatible subset of c++… seems like a perfect LLVM / clang rewriter case too, it would be easy to convert and be pure c++. Hell even a clang plugin to put the compile time into one process wouldn’t be awful. But i wonder looking at the rewrites if there’s not a terribly janky way to not need a compiler, if at some runtime cost of contextual control flow info.

It’s exactly the same to try to use pixel buds on an Apple phone too. I don’t blame Apple or Google so much as the ridiculous pissing matches of a society that refuses to find ways to cooperate efficiently. So much energy is wasted in the name of vendor lock-in and related. Would it take more energy for Google and Apple to share in expanding into the Bluetooth capabilities in a shared way? Sure for their developers, in the short run. In less than a year the society wide savings far outweighs that. Apple people might cross pollinate and buy pixel buds. Android people will get airpods. Both companies could make even more money and save us all sanity. But we are organized for short term gains. Gradient descent without knowing or using the topology of the global complex. This isn’t Apple or Google’s job to fix, not even the government. it’s an issue at the social fabric level to have deep conscientiousness… so none of this is ever gonna change in our lives.

No one is really mentioning this article in from a highschooler. Awesome job! I'm happy to read this today and really hope she will continue to see such inspiring stories and maybe some day make some.

Is there any succinct publication of his observations?

That's the only part I care about dang. I still use WSL1 and have done a number of interesting hacks to cross the ABI and tunnel windows into "Linux" userspace and I'd like to make that easier/more direct

Definitely out of date, e.g. the 3SUM subquadratic conjecture (probably 11) has been solved and improved on [1].

If it's not been already there's immediate application, e.g. problem 41.

[1]:https://link.springer.com/article/10.1007/s00453-015-0079-6

There's a book that's explicitly about this, "Program = Proof", and though it's not beginner and needs maybe a light version for earlier learners, is an excellent example.

My story: it's a joke to be a grad student. Salary in 2012: $10,800 per year without housing.

Nice! Glad to see. Huge quality of life improvement

I've really had a pet peeve about footnotes on mobile and this does the crime. If you click a footnote and it jumps very far away and doesn't have a return navigation, I have left your page usually after the second time I see a footnote and didn't note my exact scroll. A small thing but pretty please don't make me have to hunt for where I was...

Elliott Conal has to covered there: http://conal.net/papers/convolution/

I liked the way Pearl phrased it originally. A calculus of anti-correlations implies causation. That makes the nature of the analysis clear and doesn't set of the classic minds alarm bells.

Yeah I work in an FFRDC, pushing the frontier of our exploration of space. I'm quite passionate both about the employer and (most of the time) my work. If I didn't care about my employer at that level I woulda been out the door after two years. I think to myself sometimes about the other side of that though, like if I didn't care for them but the money was good.

My home hobbies resemble work within my area, but not my current job function, but I'm keenly aware my employer may try to take advantage of my other talents and do I guess the only thing that saves having an alternative hobby is that I'm so diversified that whatever my work task is I can work on an orthogonal hobby at home. It's kinda nice, I've got both really.

In my mind if I "sell out" (in terms of trading in for that sense of purpose in my work), and just work for the paycheck, then I would go for max. Work an HFT quant firm as a senior or principal engineer or research analyst. $$$. Or some other juicy gig. But I would hate myself if that became a slog and I had no time for my interests at home.

and probably no where to hide if you want to just rest and vest.

"Rest and vest". What a luxury. Some of us are trying to tread water with an anvil chained to the waist. That's what I get for choosing to work for something I'm passionate about. What a world

I think one of the reasons I have that example is that specific dynamic is cited in most planetary science texts as "de-coupled", "invariant", etc etc, when in fact it's the major casual influence here, which was quite a surprise in recent years [glances at climate mostly still beating to the tune that particle inertia does not have to care about the system angular momentum variance at the solar system scale]

The Mars global dust storm is caused by coupling of angular momentum of the (solar) system, a global a effect. The Mars system itself down to the dust does not create sufficient conditions

The idea of computing as the shared stage to reflect our own intelligence is really what sticks out to me as the best way to frame what interacting with a computer means. It's not new but Alan did a great job of motivating and framing it here. Thanks for posting this great reminder that what we use as computers today are still only poor imitations of what could truly be done if we can transport our minds to be more directly players on that stage. It's interesting to reflect the other way as well. If we are the actors reflecting a computer to itself. An AGI has to imagine and reflect in a space created of our ideas. To be native the AI needs better tools, the "mouse" of it's body controlling the closed loop of it's "graphics", how do we create such a space that is more directly shared? Dynamically trading been actor and audience in an improvisational exchange? This is the human computer symbiosis I seek.

You can run a friggin full 32 bit lisp on the untyped lambda calculus!

https://woodrush.github.io/blog/lambdalisp.html

As someone who knows not enough people care about the math, please ignore this advise and actually learn the math. You might come up with a better representation in the process. In any case you'll learn more than just it works, but how and why. And if your goal is to apply this method in other places you will have gained a good idea about how.

Yes! I am much more productive in those hours too despite being "a morning person" with regards to getting up early and being spry. On my own hobby work I find myself crushed by hitting flow at like 1 am, finally, and then oh crap I've gotta work in six hours, better get some sleep

TTY queries are written to stdout but read from stdin. That's not user interaction. E.g. if you're system doesn't have ioctl for window size (or you're over a remote serial etc), setting the cursor to the bottom right and asking it's position. Those programs break with no stdin because a tty is inherently bidirectional communication!

I may be biased as I am a trained Mathematician, but I always feel when someone says "Math is Hard", that is because they had bad teachers.

Math is easy if you build up from fundamentals, not like physics education where you say "but lets delete everything before because it had an oversimplifying assumption", rather if you build your knowledge entirely sequentially from things you know or assume, you build up a toolbag that applies literally everywhere.

So math isnt hard. Learning random bits of math out of context is hard. Climb the ladder once, you have it for life.

Hopefully for this person that sticks.

There are still bit flipping tricks like rowhammer for RAM, I wouldn't be surprised if there are such vulnerabilities in some CPUs.

Programming in dependent types with univalence (Homotopy Type Theory) is an awesome way to see this realized.

The typing statement has to be proven by realizing the isomorphism demanded by substitution. You are more than anything directly proving what you claim in the type. Since proof is isomorphism here, the computation in terms of lowering the body of the definition to a concrete set of instructions is execution of your proof! (possibly machine code or just abstract in a virtual machine like STG). The constructive world is really nice. I hope the future builds here and dependent types with univalence is made easier and more efficient.