HN user
Did the restrictions on JavaScript get resolved? IIRC, they made it so you had to use their “Ports” mechanism to interface with JavaScript, and you couldn’t write your own wrappers.
There was some drama when someone forked it so you could write your own JavaScript wrappers/FFI too?
Oooft, in cubical.ml why is your identity equivalence `CVar "__id"`? Surely this should be some fibration/reduction?
In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).
I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.
`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.
I don’t think that’s Orion specific, I have the exact same issue with Safari and Firefox
Eh. I’ve been writing a small HoTT language over the past two years based on schemes, stacks, and sites and anything short of Agda or Lean falls short in terms of Real™ Category Theory.
So much has to be pragmatised, carefully considered and made concrete categories anyway that much of the category theory exists in the documentation rather in the actual code.
There is nothing that will inherently limit AI from doing all knowledge work
Resources is one. Energy, water, cost. There seems to be diminishing returns in intelligence at the moment, whilst power and memory usage continues to go up.
Nothing a little digital lisdexamfetamine won’t solve
I don’t feel their stance is “I’m not getting enough attention and it’s all Musk’s fault and I’m leaving”.
More “X is simply not worth our time anymore”. I can’t say with any certainty that X is on a death spiral (personally it does feel that way), but the kind of crowd who have remained in spite of Musk’s many public embarrassments (and the handling of Grok deep fakes and women) probably aren’t the kind who are passionate about the EFF
A pharmacist is someone who is a chemical practitioner though?
“Man, these cryptographers didn’t know a thing about tailwind. Useless!”
Ah, but only a truly great writer could have come up with:
Start reading books or you're going to look stupid to the people around you
Wherein the prose wasn’t at all sloppy, the tautology was certainly intentional; the implied audience of “look stupid” could be to people entirely absent of the vicinity!
I was more getting at the angle that when people say things like “Wow, I asked AI to code a terminal emulator and it got it mostly right!”, it’s not because the LLM is amazingly smart only by inference, it’s been trained on the appropriated code of individuals like the above.
Mitchell Hashimoto doesn’t need LLM’s, LLM’s need Mitchell Hashimoto
Sorry, I mean verify the semantics of what the LLM has generated is exactly what you were asking for.
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating.
You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is they get backed into a corner, and they’ll do something like prove something different under the guise of another:
They’ll create long pattern matching chains as to create labyrinths of state machines.
They’ll keep naming functions, values and comments to seem plausible, but you have to follow these to make sure they are what they say. A sneaky little trick is to drop important parameters in functions, they appear in the call but not in the actual body.
They’ll do something like taking a Complex value, but only working with the real projection, rounding a number, creatively making negatives not appear by abs etc etc
So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
And when it doesn’t work, introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem.
I’ve not seen a convincing use that tactics or goals in the proof assistant themselves don’t already provide
Something running an SSH server service, yes.
A decade plus ago, you could ssh into localhost on iOS, but that got nipped in the bud with sandboxing.
Online safety act passed in the uk on 26/10/2023, aligning suspiciously close with the mysterious advent of OpenAI’s screening tool
Only if the shop assistant took your ID, photocopied it and stored it in a box marked “do not touch” under the counter, alongside transcriptions of everything you ever say inside the store.
Those pesky whistleblowers, journalists, and political dissidents have had it good for far too long. They’ve needed taking down a peg
I’ve lived in two apartments with the setup OP described, and they were both built 2003-2006. But I’ve not had it anywhere else, so it does seem constrained to a specific window of apartment developments
Other way round, no? TidalCycles predates Sonic Pi by a number of years
You can pick it up passively over time, and with your skills, if you were to actively engage then I suspect pick up the necessary very quickly, and the rest comes from experience.
I picked up Linux at 13, fortuitously just in time for the release of the Nokia 770 (later getting, and still owning the N900 too).
At that time, getting real dirty with the kernel, hardware, cross compiling etc was necessary, so 1) there were more resources 2) it was seen as mundane, busy work rather than mystical and difficult.
If I were to say how to learn the same things today, I’d probably say Gentoo is ideal - it’s insanely flexible in tinkering, has good resources on compiling the kernel and packages, and I’m a fan of crossdev for cross compiling.
Getting real dirty with hardware and electronics, the obvious answer would be one of the Raspberry Pi lineup, but if you’re very tenacious, patient and a touch unhinged, then I would actually say now’s the time to get in on RISC-V.
It’s still early days, so there’s lots of resources that have very thin abstractions between hardware <-> tooling <-> code. Devices are cheap and exciting. You’ll be on the same footing as most other people so you won’t feel like a dunce.
The cons are that a lot of RISC-V devices get shipped out with very little documentation (and sometimes only in Chinese), binary blobs making mainstream kernels difficult, and you’re learning at the same time, so you might feel you’re ice skating uphill.
Wrt to the bootloader and partition corruption; towards the twilight years of the life of the N900, when it became clear N900 had been abandoned and the N950 was still only available to select few, a bunch of smart people on the Maemo forums started reversing and writing open drivers (uboot bootloader, wifi, camera iirc), so they became pretty documented.
[..] as a design goal - to make programming fun. There was even for a while in the late 2000s the culture of _why and MINSWAN.
It was a great time - titles like Learn You A Haskell For Great Good and Land of Lisp really capture the zeitgeist.
90% manned. A lot of money and time goes into getting track access.
And collecting unmanned data is still such a pain. At the moment, you stick calibration gear to a train and hope it gets as much noise free data as it can. All whilst going at least 40mph over the area you want - you’re fighting vibrations, vehicle grease, too much sunlight, not enough sunlight, rain, ballast covering things, equipment not calibrated before going out etc etc.
Tell him that, not me; I’m simply referring to what’s on the board, above her right hand, left of her stomach. Perhaps it’s abuse of notation.
Yeah, that’s not right. I’m not sure about painstakingly… it said it couldn’t make out the notation, and spat out what it thought it could read, and you never checked it - nor read the articles for context, just assumed it was to do directly with further AI work.
It picked up on the polynomial, then what it thought was a scheme/sheaf being defined is actually the finite field with six elements. It also misread “Thue” as “the”.
If you had corrected what it read from the board, then gave it the context that he was a number theorist now working for a company trying to get AI to work through proofs, then you may have got the correct answer that this appears to be them crafting problems on polynomial reduction to test how the LLM reasons about proof.
They are expensive, but that is partly because rail workers are well paid
I must be an engineer for a different Network Rail
Agreed. In addition to yours, notions like limits/colimits, equalisers/coequalisers, kernels/cokernels, epi/monic will be very hard to grasp a motivation for without a breadth of mathematical experience in other areas.
Like learning a language by strictly the grammar and having 0 vocabulary.
Shivlov for the one and only text in linear algebra is rough. IMO, it’s a little terse and fast paced. Efficient if you’re already well versed enough to be dangerous, but otherwise I think might slow down the beginner to a crawl in places.
Same for Hartshorne’s Algebraic Geometry. Neither of these are bad textbooks at all, they both have a place on my bookshelf, but certainly better options have appeared through the years (for AG, I’d be remiss to mention Ravi Vakil’s fantastic The Rising Sea, due for a physical publishing October, and Ulrich Görtz & Torsten Wedhorn two part series)
I hope I’m not adding 2 + 2 to get 5, but it’s incredibly convenient that a lot of people are being charged for supporting a proscribed group the same month as the online safety act is rolled out…
The cynic in me almost wonders if when it comes to re-election time, these increased numbers in terrorist charges will be trotted out and the context conveniently forgotten.
I don’t think it’s dumb - hasty and premature perhaps. Manufacturers have been shipping boards with flaky RVV support, a years old kernel and undocumented blobs on in house baked OS and calling it a day.
Feels like a step towards strong arming them into shipping products that can be supported easier/not being left to rot in a drawer.
The only time a labour majority voted against this bill was when an amendment to make category 1 sites have optional controls for users (something that would have prevented this).
I’m going to guess that our MP’s are tech illiterate enough as it is, that when an opaque term like “what is a category 1” came up, someone hand waved over it and said “think Facebook or Twitter”