2026-07-17 22:32:19 <annieoxe    > Girl Scouts are hiring for VP of Agentic AI Innovation. Apply now at https://linkedin.com/jobs/view/4415733532 and build the agentic, data-driven future of American scouting.
2026-07-17 22:34:35 <xentrac     > we just got this same repugnant spam in another channel
2026-07-17 22:34:51 <xentrac     > 20:28 -!- ds9131424 [~ds9131424@67.250.60.138] has joined #bootstrappable
2026-07-17 22:34:51 <xentrac     > 20:28 < ds9131424> Girl Scouts are hiring for VP of Agentic AI Innovation. Apply now at https://linkedin.com/jobs/view/4415733532 and build the agentic, data-driven future of American scouting.
2026-07-17 22:34:55 <xentrac     > 20:29 -!- ds9131424 [~ds9131424@67.250.60.138] has quit [Remote host closed the connection]
2026-07-17 22:55:48 <tabemann    > "Agentic AI Innovation" ugh
2026-07-17 22:56:20 <xentrac     > I think this is some kind of scam
2026-07-17 22:56:36 <tabemann    > the job spam, likely yeah
2026-07-17 22:56:37 <xentrac     > because I'm skeptical that the Girl Scouts would hire a recruiter to spam IRC for them
2026-07-17 22:57:12 <tabemann    > but even if it *weren't*, the phrase "Agentic AI Innovation" is all kinds of "ugh" to me
2026-07-17 22:57:30 <lofty       > AAII
2026-07-17 22:57:33 <lofty       > :p
2026-07-17 22:57:45 <tabemann    > it's corporate hype machine-arrhea
2026-07-17 22:58:49 <tabemann    > there's only one thing I've ever seriously considered using "Agentic AI" for, and that is to update SDD docs that are a PITA to update that no one really reads
2026-07-17 22:58:58 <xentrac     > I'm in favor of innovation, generally speaking, and I'm very curious to see what's going to come out of AI, in part because it might kill me, and the "agentic" experimentation seems to be what's currently most promising, but the idea of a "VP of Agentic AI Innovation" makes me think that someone is acting on some fundamental misunderstandings
2026-07-17 22:59:32 <xentrac     > hmm, well, you might have heard that different AI companies resolved 10 open Erdös problems a few weeks ago
2026-07-17 23:00:14 <tabemann    > at my current job, the only thing I really use "Agentic AI" for is to write a "Hello World" program in Python once every few months, so I am officially on my company's list of "people who use agentic AI"
2026-07-17 23:00:16 <xentrac     > mostly using Lean, so it doesn't matter if nobody reads what the agentic AI writes; Lean has checked it
2026-07-17 23:01:03 <tabemann    > from what I've heard, though, AI-generated proofs are often nigh-unreadable, and require significant revision by humans before humans can really parse them
2026-07-17 23:02:27 <xentrac     > there are different points of view about what a proof is for
2026-07-17 23:02:39 <xentrac     > some people believe that it's to establish the truth of a theorem
2026-07-17 23:02:43 <tabemann    > I *still* remember the time where I was burned hard by accepting some code generated by a coworker with GitHub Copilot, where it contained a key bug that I missed in reviewing the code because I wasn't familiar with the API it was using so I didn't know that it misused the API
2026-07-17 23:02:50 <xentrac     > if that's the case, humans parsing them is unnecessary
2026-07-17 23:03:04 <xentrac     > what matters is humans parsing the formalization of the problem
2026-07-17 23:03:37 <tabemann    > wasted half a day banging my head on the bug when I would have been done in half an hour had I just gone and read the API docs and written it myself by hand
2026-07-17 23:03:49 <xentrac     > yeah, I've had that experience a lot
2026-07-17 23:04:15 <xentrac     > you can spend half an hour doing what would have taken you half a day, and then half a day doing what would have taken you half an hour
2026-07-17 23:04:20 <xentrac     > it's like playing a slot machine
2026-07-17 23:05:58 <tabemann    > the other thing is that in proper 'software engineering' spewing out code is only a small part of your job -- and hand-writing code, while taking longer than having an AI generated it for you, makes the rest of 'software engineering' processes so much easier than with AI
2026-07-17 23:06:09 <tabemann    > *generate
2026-07-17 23:06:25 <tabemann    > e.g. hand-written code is much easier to debug and code review
2026-07-17 23:06:47 <xentrac     > a lot of proper 'software engineering' in my experience is reading code, and I've found LLMs to be much better at that than they are at writing it
2026-07-17 23:06:48 <tabemann    > and less hand-checking of each line of code is needed because you know what you wrote
2026-07-17 23:08:32 <tabemann    > usually when I hand-write code the main bugs I make are simple typos or thinkos and it just works after some cycles through the compiler and correcting errors caught in the process
2026-07-17 23:08:50 <xentrac     > oddly enough, LLMs explaining a code base to you so that you can write the code doesn't seem to have been a workflow that has caught on much
2026-07-17 23:09:44 <tabemann    > even in Forth, where the compiler protects you far less than it does in C++ (my main language at my day job), after a few runs and subsequent staring at code I can figure out where I'd made my mistakes and fix them
2026-07-17 23:10:48 <tabemann    > I personally like reading code, which, yeah, is a big part of any proper 'software engineering'
2026-07-17 23:11:22 <tabemann    > oftentimes, when I do run into bugs, I simply stare at my code for a while and the source of the bug eventually pops out at me
2026-07-17 23:11:38 <xentrac     > I don't think that's true
2026-07-17 23:11:44 <xentrac     > sorry
2026-07-17 23:11:54 <xentrac     > specifically what I don't think is true is this:
2026-07-17 23:12:13 <xentrac     > "after a few runs and subsequent staring at code I can figure out where I'd made my mistakes and fix them"
2026-07-17 23:12:21 <xentrac     > that is not true of you nor of any other human being
2026-07-17 23:12:31 <tabemann    > what I'm doing when staring at the code oftentimes is executing it in my head
2026-07-17 23:13:04 <xentrac     > if it were true, people like you (even if there weren't very many of you) would consistently ship bug-free code
2026-07-17 23:14:12 <xentrac     > in real life, even the best-tested and best-reviewed code, such as the Space Shuttle in-flight software, has bugs discovered in it that have remained unnoticed for decades
2026-07-17 23:14:36 <tabemann    > when I do write code which repeated compiling and staring doesn't solve, it's oftentimes because something in my underlying design in head was wrong
2026-07-17 23:14:49 <tabemann    > some underlying assumption
2026-07-17 23:14:54 <tabemann    > some underlying logic
2026-07-17 23:15:22 <tabemann    > those are the hard ones, and often lead me to tearing up my design and starting over or at least doing a significant rewrite
2026-07-17 23:15:45 <xentrac     > qmail is close to bug-free, but still Georgi Guninski found three bugs in it in 02005 which had lain undescovered for 8 years: https://lwn.net/Articles/820969/
2026-07-17 23:16:34 <xentrac     > I would agree with a weakened version of your statement: "after a few runs and subsequent staring at code I can figure out where I'd made *most* *of* my mistakes and fix them"
2026-07-17 23:16:59 <tabemann    > in many cases, outstanding bugs result from use cases I had not anticipated
2026-07-17 23:16:59 <xentrac     > but those can be vastly different statements in practice
2026-07-17 23:17:39 <tabemann    > where I covered my assumptions in my tests, but in another scenario I'd never'd anticipated those assumptions do not hold somehow
2026-07-17 23:19:00 <xentrac     > yes
2026-07-17 23:19:52 <xentrac     > some of these are things that can show up as misformalizations in proofs
2026-07-17 23:20:07 <tabemann    > in general, though, most bugs to me are either rather shallow or very deep -- either superficial fuckups, or fundamental design errors
2026-07-17 23:20:10 <xentrac     > others are things that formal methods routinely discover
2026-07-17 23:22:05 <tabemann    > the problem with formal methods is that they require you to be a mathematician, and even if your proof is correct, how do you know that the problem you are solving is actually the right problem?
2026-07-17 23:22:42 <tabemann    > because in many cases deep issues involve correct implementation of the design, but the problem the design seeks to solve is itself wrong
2026-07-17 23:23:36 <tabemann    > aside from the part that I'm not a mathematician, part of my personal skepticism of formal methods results from the above
2026-07-17 23:25:35 <tabemann    > as Knuth once said, "Beware of bugs in the above code; I have only proved it correct, not tried it."
2026-07-17 23:26:26 <xentrac     > it seems like possibly you didn't understand what I was saying above
2026-07-17 23:26:46 <xentrac     > because you just restated parts of it!
2026-07-17 23:27:36 <tabemann    > I misread part of what you said
2026-07-17 23:27:38 <xentrac     > there's a significant difference today from when Knuth wrote that, though
2026-07-17 23:28:27 <tabemann    > I read "misformalizations" as meaning bugs show up in the process of formalization, when you'd meant that there are bugs that are incorrectly encoded as "correct" in the formalization process
2026-07-17 23:28:30 <xentrac     > at the time, the only way to check purported proofs of correctness was for human mathematicians to read them
2026-07-17 23:28:35 <xentrac     > yes, exactly
2026-07-17 23:29:14 <xentrac     > misformalization is when your formalization of a theorem you want to prove doesn't correspond to the theorem you actually want to prove
2026-07-17 23:29:52 <xentrac     > so your eventual formal proof proves the wrong thing
2026-07-17 23:30:07 <tabemann    > much of the time when I run into a deep bug, it's because I correctly implemented the wrong thing
2026-07-17 23:30:13 <xentrac     > exactly
2026-07-17 23:32:50 <tabemann    > and this is also a problem with testing, because your tests themselves make assumptions
2026-07-17 23:33:14 <tabemann    > and if your conception of the problem is wrong, your tests themselves will likely be wrong too
2026-07-17 23:33:27 <xentrac     > yes.  I've found generative testing with things like Hypothesis to be an extremely useful upgrade to my testing practice
2026-07-17 23:34:00 <xentrac     > but stating the properties you want the generative testing framework to test is just the formalization problem again
2026-07-17 23:34:12 <tabemann    > yeah
2026-07-17 23:34:30 <xentrac     > it can still be very valuable in forcing you to state your assumptions thoug
2026-07-17 23:34:33 <xentrac     > *though
2026-07-17 23:35:17 <xentrac     > because if you forget to state something like "this parameter is a positive number" or "this parameter is less than 2³¹" or "this character is printable ASCII" the generative testing framework will flag that immediately
2026-07-17 23:36:31 <xentrac     > misformalization is more dangerous when it makes your formalization incorrectly narrow than when it makes your formalization incorrectly broad, because the latter results in immediate failure
2026-07-17 23:38:15 <tabemann    > at my day job we're running into very empirical testing matters because we've been forced to cut down on RAM usage (both bytes and RAM channels) due to the RAM price issues, and we have to downscale our algorithms to fit in a smaller amount of RAM or not spend inordinate amounts of time when forced to run with fewer RAM channels, but we don't have any truly formal models of RAM utilization, whether
2026-07-17 23:38:17 <tabemann    > in bytes or in time
2026-07-17 23:38:29 <xentrac     > yeah, that's a big problem
2026-07-17 23:39:42 <tabemann    > basically what we've ended up having to do is eyeball it by prescribing ridiculously large prescriptions, and then verify that it doesn't exhaust RAM on the smaller configuration or take too much more time with fewer RAM channels
2026-07-17 23:40:49 <tabemann    > and say "because this prescription which is ridiculous doesn't cause a failure with our restricted configuration, we know that non-ridiculous prescriptions will probably be /okay/"
2026-07-17 23:40:55 <xentrac     > what are channels?
2026-07-17 23:41:01 <tabemann    > RAM channels
2026-07-17 23:41:09 <xentrac     > yeah
2026-07-17 23:41:30 <lofty       > presumably a set of I/O for a DIMM
2026-07-17 23:41:32 <tabemann    > we started out with 16 GiB DIMMs, then were forced to 32 GiB DIMMs, and now are forced to 64 GiB DIMMs
2026-07-17 23:41:52 <tabemann    > each doubling of the size of a DIMM is a halving in the number of channels
2026-07-17 23:42:23 <tabemann    > so the same RAM size with 16 GiB DIMMs is faster than with 32 GiB DIMMs is faster than with 64 GiB DIMMs
2026-07-17 23:42:32 <xentrac     > oh, interesting
2026-07-17 23:42:48 <tabemann    > the problem is that the AI people were first buying up all the 16 GiB DIMMs, and now the US gov't is buying up all the 32 GiB DIMMs
2026-07-17 23:42:52 <xentrac     > yeah
2026-07-17 23:43:07 <tabemann    > so we're forced to use 64 GiB DIMMs
2026-07-17 23:43:22 <pyzozord    > 02hey i'm thinking about transpiring a concat language like forth to c, and i was thinking about converting each word to just a number and then started wondering how many bits i need to have enough to enumerate each unique words. So im wondering... how many unique words does the largest forth program you ever saw had?
2026-07-17 23:43:30 <xentrac     > I didn't realize that the memory bandwidth on current CPU sockets was enough to saturate even a single DIMM
2026-07-17 23:43:44 <xentrac     > but I guess you might have like a lot of CPU sockets?
2026-07-17 23:43:59 <tabemann    > thing is, while the jump from 16 GiB DIMMs to 32 GiB DIMMs results in a smallish loss of performance, the jump from 32 GiB DIMMs to 64 GiB DIMMs results in a significantly greater loss of performance
2026-07-17 23:44:01 <xentrac     > pyzozord: tens of thousands?
2026-07-17 23:44:03 <lofty       > pyzozord: 8 bits probably isn't enough, 16 bits is very definitely enough
2026-07-17 23:44:24 <pyzozord    > 02hmm
2026-07-17 23:44:24 <xentrac     > I wouldn't say *very* definitely, but probably
2026-07-17 23:44:44 <tabemann    > xentrac: we're using two CPU sockets currently, but are considering reducing to one CPU socket if the CPU market gets too expensive
2026-07-17 23:46:44 <tabemann    > oh, to answer your question from earlier, a RAM channel is a lane of communication between a CPU and a DIMM
2026-07-17 23:47:13 <tabemann    > so going from, say, 32 GiB DIMMs to 64 GiB DIMMs for the same amount of RAM is roughly halving the RAM bandwidth available
2026-07-17 23:47:26 <tabemann    > with otherwise equivalent DIMMs, that is
2026-07-17 23:48:57 <tabemann    > (just for the record, I work in biomedical, MR reconstruction to be exact, where in some use cases we really push things like RAM and RAM channel utilization)
2026-07-17 23:52:45 <tabemann    > outside my day job I'd normally consider 128 GiB to be a lot of RAM, whereas at my job to me it's only a 'reasonable' amount of RAM but not a lot
2026-07-17 23:53:36 <xentrac     > nuclear magnetic resonance?  where you're doing Fourier transforms but, sometimes, not the fast kind?
2026-07-17 23:54:13 <tabemann    > MR imaging
2026-07-17 23:54:39 <tabemann    > "NMR" when I hear it is usually used by people who aren't scared by the word "nuclear", e.g. NMR for chemistry
2026-07-17 23:55:04 <tabemann    > we use FFT's a lot in what we do
2026-07-17 23:55:30 <tabemann    > e.g. our input data is all in K-space, and we have to shove it through an IFFT to get image data
2026-07-17 23:55:55 <tabemann    > and we do certain sorts of transforms where we convert back and forth between image space and K-space
2026-07-17 23:57:47 <tabemann    > in what I was doing some years ago I was heavily involved in transformations of that sort; what I've been doing in the past two years has been all in image space, though
2026-07-17 23:59:21 <xentrac     > heh, but nuclear magnetic resonance is what you mean, right?  Not, for example, Mineral Resources, mental retardation, mitral regurgitation, or magnetoresistance?