smj-edison

6 ms·

91.
by smj-edison 6mo ago
Plus backups should be time gated, where the software physically blocks you from removing backups for X days.
92.
by smj-edison 6mo ago
On the point of avoiding the struggle of learning, I think it's easy to swing too far the other direction and go back to not using modern development tools. I think it is doing a new learner a disservice by saying something like "
93.
by smj-edison 6mo ago
Dang, this is really relatable. A couple months I started digging into the Jimtcl interpreter, which is a 20-year-old Tcl interpreter written in C. My goal was to make it thread safe, which I naively thought wouldn't be that hard. Turn
94.
by smj-edison 6mo ago
Thanks! I can pass it on. Would you say then that having an overview on the main page, with links for more details would be a better approach?
95.
by smj-edison 6mo ago
I will say scanners are somewhat unergonomic, but if you had a high enough definition camera, you could photograph the document in its "natural environment". Granted, it's harder to get an evenly lit picture that way, but I t
96.
by smj-edison 6mo ago
And a shout-out to https://folk.computer/ as well! They're not as far along in terms of feature parity, but they are open source, and exploring the space in other directions.
97.
by smj-edison 6mo ago
That's a fair question, and looking at my post I now realize I have two independent points: 1. A proof mindset is really hard to learn. 2. Writing theorem definitions can be hard, but writing a proof can be even harder. So, if you coul
98.
by smj-edison 6mo ago
I'm curious to see if formally verified software will get more popular. I'm somewhat doubtful, since getting programmers to learn formally math is hard (rightfully so, but still sad). But, if LLMs could take over the drudgery of w
99.
by smj-edison 6mo ago
Chronic tiredness can be such a hard thing to figure out, sorry you've been going through that! Is it sleepiness (as in can fall asleep at any point of the day), or fatigue (as in non-restorative sleep, brain fog, feeling exhausted, et
100.
by smj-edison 6mo ago
Not OP, but this is my script: https://gist.github.com/smj-edison/33229537007a73520a26a14a0... It's been cobbled together over the years to add things I want, like not backing up on battery, or sending a desktop m
101.
by smj-edison 6mo ago
Side note, but this product looks really cool! I have a fundamental mistrust of all boolean operations, so to see a system that actually works with degenerate cases correctly is refreshing.
102.
Metamath C(github.com)
2 points by smj-edison 6mo ago|0 comments
103.
by smj-edison 6mo ago
Not sure if you're into 40s music, but there's a little known instrument called a theatre organ. It was conceived when silent films were taking off, and theaters needed some form of background music. Paying an organist was much ch
104.
by smj-edison 7mo ago
> I happen to prefer big endian systems in my own development life because they are easier for me to work with, especially reading crash dumps. If hex editors were mirrored both left to right and right to left, would it be easier to read
105.
by smj-edison 7mo ago
Huh I hadn't paid that much attention to MMC, but this looks fascinating! I don't like how fragile SMT servers are, so to be able to use tactics and proof techniques would be really powerful for formal verification. Also, to be ab
106.
by smj-edison 7mo ago
The description of working with AI tools really resonates with me. It's dangerous to work on my codebase when I'm tired, since I don't feel like doing it properly, so I play slots with Claude, and stay up later than I should.
107.
by smj-edison 7mo ago
As someone who has only dabbled with FPGAs before, this is incredible to see all the steps end-to-end for silicon development! I feel like the articles I've read always leave out details in one part or another, so it's interesting
108.
by smj-edison 7mo ago
I feel the same. When I first heard about metamath I was blown away at how I could drill down to the base axioms (I had only tried Lean before). Lean also feels too magical for my taste, and I dislike that I don't have a good mental mo
109.
by smj-edison 7mo ago
It's interesting to see a lot of formalized proofs gather around Lean (specifically Mathlib). I've in a formal math class right now, so it's a bit weird learning ZFC while messing around with Lean, which is based on dependant
110.
Sparkle HDL(github.com)
2 points by smj-edison 7mo ago|0 comments
111.
by smj-edison 7mo ago
I use vanilla Claude Code, and I've never looked that much into skills, so I'm curious: how do you know when it's time to add a new skill?
112.
by smj-edison 7mo ago
Don't most people use C++11 atomics now? You have SeqCst, Release, Acquire, and Relaxed (with Consume deprecated due to the difficulty of implementing it). You can do loads, stores, and exchanges with each ordering type. Zig, Rust, and
113.
by smj-edison 7mo ago
That's fair, since you can leak the box. I will say though it's not as ergonomic as defer, as defer handles all exits from the scope, where it's trickier to juggle destructors. Though on further thought, I suppose the arena c
114.
by smj-edison 7mo ago
The problem is it only takes one bad or incomplete API needed for your specific use case . I ran into this a lot when I used cpal. For example, the data stream enum type (i16, u8, f32, etc) didn't have Hash or Eq derived, so I had to
115.
by smj-edison 7mo ago
Agreed. > Mathematical concepts need not necessarily have any practical or real-life applications (pure mathematics), but it's a worthy pursuit on its own. I guess I always had a sense that this was true, but taking a formal proofs
116.
by smj-edison 7mo ago
I feel like encapsulation and composition are in strong tension, and this is one place where it boils over. I've written a decent bit of Rust, and am currently messing around with Zig. So the comparison is pretty fresh on my mind: In R
117.
by smj-edison 7mo ago
Crap, you're right. I swear, tiny usernames is both a boon and a curse... > Personally, I work in games. So pretty much everything in the discourse of LLMs and Gen AI has been amplified 5x for me. The layoffs, the gamers' react
118.
by smj-edison 7mo ago
I don't read it as superiority, perhaps bitterness would be the closest word to what I'm reading. > sometimes you have to call people out on their BS That's true, but I think that it's often much later than what some
119.
by smj-edison 7mo ago
> Get me a job Heh, I'm a college student, so I can't help with that... You could also try Gemini 3 pro with Gemini's CLI which is free, though it's not as good at using tools. But, it sounds like you're not inte
120.
by smj-edison 7mo ago
I'm working on an interpreter right now, and I'm considering adding JIT support in the future. Are there other blog posts like this, or deep dives that talk about how to implement and tune a JIT?

More ›