boxfire

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.

Damn. One of the most powerful experiences of my life was working for someone with ALS. They could only communicate via moving and blinking their eyes slightly as I cued them. This person pivoted their career and was actively researching the disease locking them into their brain.

One day they played a trick on me (I was basically a human auto complete as I took some graduate courses in their field and I was able to help finish the proposal they were writing). They made a joke in the word document. It made me laugh, and as I was looking in their eye I could see the joy that made. I cried so much that night.

It really really gets to me. Every time I saw a new eye tracker device or otherwise I would email their spouse. I fuckin hate that disease, but I'm amazed at the human spirit I've seen it reveal.

Ugh the first paragraph kicks off with a missing bit of information. Min Nan has at least 5 subvarieties. In my spouse's it's pronounced "de" not "te" (and she is Min Nan as a first language). She laughed and said there's no way the people in Xiamen said "te", or any of the subvarieties she is familiar with within coastal fujian where she spent the first 25 years of her life.

So failed look at archaic miss transliterations, kind of reminiscent of the entire theme of the article. The example map being built on an argument from a bad assumption (a historical error as a pretext for argument).

Perfect irony.

3090 does 4x nvlink each way, ~100 GB/s bidirectional data

Scroll scroll scroll and...

https://arxiv.org/abs/2303.15412

Do check this discussion the other day: https://news.ycombinator.com/item?id=34816184#34826067

She and yes this is right.

Wish I saw this write-up in like 2009. The terminology in Cohomology was pretty opaque to me until I (much later) learned the concepts via a backwards mapping from learning deeper applications of algebraic geometry. I would have learned that much easier if I understood this easier.

Would this model offer improved predictions for the SGP and SDP models used in Two Line Element ephemerides for satellites?

Yeah I chuckle every time people keep rediscovering Hilbert's functional analysis and the idea of orthogonal basis for functional spaces (goes well beyond Hilbert's widest dreams too!!).

Also Re the person who said no to you... Wave mechanics is written in Hilbert's language directly...

Which is prescient... this is a tool by the NSA after all. I would be disappointed if it wasn't back-doored... Anybody working on a feature-parity FOSS alternative from scratch?

Agree on the density, also initially I had that cool holographic cover facing out the open side of my bookshelf to the living room until one night a passing headlight beamed across it in the dark and I realized how absolutely incredibly creepy it was to have Lick as sudden posthumous voyeur...

On the idea and content, it reveals to me there was a great shadow world of ideas in those early days I think are still being "rediscovered" in the current time. We did an awful job of following through on visionaries like him, hell even Grace Hopper's simple 1955 paper on compiler thru compiler compilers didnt make a comeback until the shadows of the 70's, then 90's, and the past decade.

We imagined the world in the 50s. We invented it in the 60s. And then we entered a profit-driven dark age that is barely letting those results trickle into everyday reality. The future of computing is so far from what we conceptualize today we still don't even have the vocabulary for it. Conceptually this essay lays it out.

Try synthesizing a toy program in Idris2 with a lsp server and querying the compiler about what you are writing as you explore. It will open your eyes that we have just hit this reality. Don't be fooled by copilot, its the cheap plastic copy of real intelligence working with computers alternating their best strengths.

It's very worth pointing out and in fact advocating for the compiler options -fwrapv and -ftrapv

Which both make signed integers take the expected two's complement behavior, or traps signed integer overflow, respectively.

N.B. left shifting into the sign bit is still undefined behavior... On x86-64 gcc and clang seem to perform the shift as if the number is interpreted unsigned, then shifted, then interpreted signed.

Just wanted to point out at JPL there are many 25-year-old people commanding spaceships, rovers, and landers. Sometimes room-fulls of them. Not a great example.

> However, just a couple of months into my project, I figured out, I wouldn’t find anyone to discuss my research with: My supervisors have a rather superficial understanding of Quantum Computing, and I feel like their idea to start a project in that domain was to a not inconsiderable extent motivated by the prospect of granted research funds, not primarily by their desire to achieve a deeper understanding of quantum stuff.

Sounds very familiar. I saw this a lot in grad school. My first advisor was also fed up with the nature in academia and left tenure path to work in private industry, leaving me to fend for money in this vein.

So then my graduate research topic came into this line. I stopped that after I realized that not only was it fishing far off the path of my social support, it was also weapons research disguised via a friendly sounding problem.

I switched programs, to an advisor who seemed to want me to work in something he actually does. Then I had zero relationship with him and became basically a highly underpaid developer to crank out the numbers that corroborated his research at 100+ hour weeks. In the marginal time I was tying to figure out if I could somehow make the small corner I thought might make a thesis fit into his unspoken program. I got the hint that my PhD was predicated on making his research stand up, and having a part in it is what my PhD would represent, not any actual original work.

I became a little more cynical but continued, now paying much more attention on the side to other's experience. I found this was nearly universal from 'top schools', and then with the overflow of candidates to academic jobs they take this style to the next tier of schools where they get tenure by making a lemming line of candidates do the same.

At this point it was the breaking point. I had a great internship the previous summer. I had a "come work for us now or maybe never" ultimatum. I took the plunge.

ABD Twice. And that I consider a great accomplishment that I am quite proud of.

That second Mars Rover with plutonium is Perseverance, not Opportunity. Oppy was solar and lost to the great dust storm of 2018.

Moreover this doc makes it more apparent how much he waxes without real references: https://ntrs.nasa.gov/api/citations/20090007797/downloads/20...

> Routine calculations were made using slide rules. More complex calculations, such as stress analysis, required Friden mechanical calculators.

Fascinating read. No the SR-71 didn't appear out of thin air in a sprint of intensity unheard of on earth to date. Turns out after the U-2 taught us so much we said let's make a higher, faster U-3 and then spent a decade on that concept in a series of designs and tests.

I really wish that this kind of cherry-picked mythos building fact wasn't what made half of what built the perception of good engineering to most of my present and future colleagues.

I read the article hoping to see examples of reasoning that the slide rule instilled.

It reads more like a jealous rant than anything else. He fails to cite why those plans developments were so fast (hint it wasn't the magic of a slide rule.... It was a decade of design and test in products before the one with the name he assigned all credit to)

He also has a sort of confirmation bias here, failing to note things we could not have possibly done without computers. Try a Martian sky crane landing without atmospheric modeling ha ha.

Anyone have a reference for rules of thumb type thinking or other insights that come from slide rules?

The top post on HN when I last checked was about Mercedes removing all liability from the driver while it's engaged. When I first read that I imagined all the people who would have stories like this. This is the second link I opened, it was number 6. These lawyers must fear consequences for allowing more stories like this to happen.

Not knocking the significance of this, but there are a lot of 'answers' that would get a straight up F for a university test:

> Original Question: Let rands denote the two real roots of x^2−x√(5 + 1) = 0. Then determine r^8+s^8.

> Codex Input: Calculate the roots of $xˆ2 - x \sqrt{5} + 1 = 0. Call the two roots r and s. Calculate z = rˆ8 + sˆ8. Evaluatez as an integer. Use sympy.

> Codex Output: > from sympy import * > x = Symbol(’x’) > r = solve(x*2 - xsqrt(5) + 1, x)[0] > s = solve(x*2 - xsqrt(5) + 1, x)[1] > z = r*8 + s*8 > print(z.evalf())

> Solution: 47

If the solution did not have the derivation of the algebra, the solution is wrong in university math. Now solving these problems for application, this is quite interesting and powerful.

Demonstrating understanding of why we get to the solution IS mathematical reasoning (at this level). This paper demonstrates being able to leap across mathematical reasoning, but not the reasoning itself.

MD5 is a 128 bit random number no one would ever have thought would collide. 64 bits is peanuts especially when message types are being defined dynamically

This architecture was also used in the link referenced when bringing up alternative implementations:

https://github.com/google/mediapipe/issues/877#issuecomment-...

> But who's going to work without AC (other than crazy HoTT people)?

Yeah... Those crazy HoTT people, trying to actualize the goal of putting mathematics on an actually firm foundation and removing the rest of the gobblygook handwaved into the religion of math as opposed to the pure logic it represents...

Also you can use HoTT WITH AC / law of excluded middle... It's just not there by default and there are some really nice things you get without it, so it's pretty much only the lazy crutch of mathematics since forever. If you see proof via excluded middle, consider it a code smell (and recall by the Curry-Howard correspondence the proof is essentially code)

So what happens when someone makes a transformer network that can read fanfics and animate them live trained from the whole collection of MPAA movies? I mean its inevitable. Given the history of the MPAA, I don't think they're gonna lie down and just take it. I feel like we're in a slippery slope to provoke the "IP lords" into brutally draconian measures that will make the Disney copyright extensions look like a tax deferral.

Nice this does the job, probably could be done more efficiently, but I like that its not a kitchen-sink library. Unfortunate that the data generator is certainly not "clean C"... perl, ruby, and julia, all to generate character width table? Ugh. Otherwise this lib does a pretty good job. Thanks for the reference!

edit* Yikes https://github.com/JuliaStrings/utf8proc/blob/master/utf8pro... Still this is a good template to maybe cut a (safter) state-based iterator out of their logic...

5th bullet of "Who is this library for?" at the top of the documentation [1] had me excited:

> you want to work with higher-level primitives (code points, graphames) when iterating text that do not break your text apart;

In reality grapheme clusters are implemented nowhere and are only in the glossary. I wanted to see how this handled the sprawling complexity that can beget.

Someone call me when a library can iterate in that form, which isn't written by committee.

[1]: https://ztdtext.readthedocs.io/en/latest/

Okay so this is one thing that boils me about quanta magazine. The authors obviously have enough background in mathematics to know the nature of the field, yet they do these very long winded, vague intros, which serve to mystify the subject and build it up. That is a major disservice to the knowledge itself. Sure you can't drop the mathematical definitions in the front, but your thesis paragraph can say least say the names of the major branches you're unifying without having to read half the article. Holy moley, everything is written to waste our attention on suspense and it's driving me wild. Where's the dry but laymen-approachable math and physics publication at? Oh yeah that doesn't sell time in the face of ads.

To not invent new ambiguities I would phrase this succinctly as the solution having intrinsic complexity vs extrinsic complexity.

I wonder what kind of placement accuracy that arm gets, both relative and absolute? Seems like that arm is doing better than I would expect for the size/weight of the actuators. Not something you'd be able to do without an extremely expensive arm.