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