In the last company I worked at, when a project was major enough (read, long-running and full of tricky details) to require two devs' full-time attention, they'd hole up in a flex room for weeks at a time.[0] "The cave" basically became their temporary office until they'd re-emerge ~a month later.
I spent a few weeks in the cave and it was surprisingly chill, not nearly as oppressive as it sounds. (Although, I was much more energetic a decade ago and maybe it wouldn't be quite as fun these days :-P.) I still have a picture of my madness-induced, Git hook–infested scribblings....
[0] The team's usual room was an open floor plan, which was fine with good headphones, but naturally that solution doesn't work for pair programming.
If I reached the video from the recommendations on another video/the YT homepage, I'll go back and select "Not interested" there. It's not foolproof, especially b/c the back button will still cause YouTube to update the original page (and so the previous recommendation can disappear entirely), but anecdotally this strategy seems to work pretty well.
> you need to review only the lines that correspond to the theorem that you want to prove and their types
This is (unfortunately) not actually the case—just a few weeks ago, someone "proved" the Collatz conjecture via a Lean proof 1) whose theorem statement was correct, 2) typechecked, and 3) was even verified by external tools with their own implementations of the kernel.[0]
The problem was (AFAIK) that the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective (I don't think Lean is unique in this regard; pretty sure Rocq and Agda are in a similar situation). And so when the kernel implements some feature whose soundness isn't guaranteed, the independent verification tools (or at least some of them) follow suit, and now any issues in the former affect the latter as well.
Huh. Thanks for bringing that into my attention, and the link!
Yes, in hindsight it makes sense that a eager LLM would exploit bugs in the kernel itself. I have not read the details yet (but want to!) and assume that it is rather related to the layers directly before or after the type-theory core; i.e. that the AI managed to get a correct typecheck by sidestepping a check during in one of the translation steps somehow, by manipulating the kernels result or by going totally hacker mode and swap implementation/overwrite memory; that is just speculation on my part though, I mainly base if on what I know about Haskell and the https://en.wikipedia.org/wiki/Calculus_of_constructions in general that have not that many constructs, and I would assume the variants used in Rocq and Lean are proven sound.
For experimental features where soundness is not proven, all bets are off IMO, but of course, that does not stop bad actors from engagement knowlingly abusing unsoundness for their own gain. Fortunately, that kind of manipulation is easy to verify when one has access to the codebase; I am would assume that something like lints for experimental features exist, or better even, something like a "sound mode". That does not help against hacking the kernel machinery though.
Concluding notes:
- In this particular instance, the Collatz conjecture was appearently chosen on purpose to demonstrate the Kernel bug, from the same thread: "Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem."
- IF the code is made public (and it would be highly suspicious if parts of a proof where hidden), then I would assume this kind of hack is 1) easier to spot that other kinds of hack, since the asset-under-attack is really small and 2) there is not so much incentive to use much time/ingenuity/tokens on finding those hacks (the more are found and fixed, the better of course) 3) and they should be easy to defend against, I would assume; my first thought would be the flag I mentioned above that simply forbids all non-sound features, at the cost of limiting expressive power.
----
Edit: I checked, and I think it alleviates my worries in the sense that the bug(s) where not in the type theory or its implementation, but rather the machinery around it. Further context below:
The following is from that thread or links from it:
- "Fixes two things: (1) more strict/nuanced handling for structure/proj interactions, and (2) adds methods for enforcing that generated auxiliary data for inductives, constructors, and recursors are more strictly checked against the assertions in the export file." | That is the fix to the non-Lean-kernel that was mentioned. To me, (2) looks firmly like what I meant with "supporting machinery", regarding (1), I do not know enough to have an opinion about it (i.e. how on what layer those interactions happen(ed)) | https://github.com/ammkrn/nanoda_lib/pull/22
- "For example, pipeline wedges (execute this instruction and the core freezes and never executes another instruction) would not be found by these techniques..." | Power and limits of Lean | https://infosec.exchange/@david_chisnall/117003914014196496
- "@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it. There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer." | Computer-checked proofs run on computers, which brings its own attack vectors, independent of how well the kernel is written | https://infosec.exchange/@0xabad1dea/117002712346315184
personal, cautios takeaway after reading the details: If you use Lean4 to write proofs, or read that a reputable group of mathematicians publizised a Lean4 proof, you are still highly unlikely to be fooled by a bug, and if Fable 5 decides to exploit a 0day in the core Lean4 machinery, that should still be able to be caught quickly.
But this means you're "abusing" dark/light mode to signal unrelated information. If some visual customization (theme, font size, etc.) happens to allow you to do something like that, then of course more power to you, but I don't think it has any relevance to the design of the thing itself. It just seems unreasonable to me to expect designers to consider all the ways their designs could do double-duty for any given user (cf. "every change breaks someone's workflow").
I was just supplying one reason for changing it, other people may just prefer some particular site or application in light mode versus dark (and vice versa) instead of managing multiple instances of the same thing like I am. Suppose you're editing documents and your word processor has dark mode, but you want it to always be in light mode. With the described control in the article you would have to change the behavior in the evening, specifically, to get it to stay in light mode permanently (or change your system settings to be opposite your normal settings, switch it to light, and then switch your system settings back).
There is no way any one with any common sense can think that this two-choice option (one is magic, one does what you would expect; which is which depends on time of day for many users) is better than a three-choice option where each choice does exactly what you'd expect.
> Suppose you're editing [...] but you want it to always be in light mode.
Your whole objection here hinges on you coming to that realization during the day when it's already in light mode by default. The 99.9% likelihood of "When does a user decide to go looking for the dark/light settings?" is "when the current color != the color desired. For your above scenario you'd go in there the first time you used your word processor at night. You'd flip it exactly once, and it would do what you described you want - stay light forever.
Perhaps you're the kind of nerd like me who likes poking through and tweaking every available setting of an app proactively, just for fun... and I'd expect VS Code for instance, to be optimized for "us." But the vast majority of people would never go hunting for the setting to "make it always light" at the time when it's already light. The thesis here is that, for apps not designed for developers, it's probably more valuable to not have those who aren't nearly as expert have to wonder if they're picking the wrong choice by offering a third option.
But this change breaks functionality for some people, without correspondingly improving anything for others. So what's the point?
In my experience, software that is designed to work only for the most average user ends up feeling terrible for most everybody, because most people deviate from the average in one way or another, at one time or another.
It feels especially bad when the software makes assumptions about what the user wants, to the point of including a button that doesn't always do the same thing when pressed, and which doesn't even tell the user it doesn't always do the same thing when pressed.
Just look at all the complaints Microsoft gets for the way Windows constantly reverts or ignores user settings.
Or the way it feels to google a very specific set of search terms, only to receive back 20 completely irrelevant listicles that answer a statistically more likely question you didn't ask.
Put yourself in the shoes of someone who has no idea what systemwide dark and light mode settings are. There is exactly one reason they are seeking out this control: "It's in dark mode and I want it light" or "It's light mode and I want it dark."
The improvement for them is that when they get here and see "Dark, Light, System" with System selected, they wonder "What's System?" Is System important? Will I break something if I change it from System? Is this even the right setting or is this something else? If I want it changed back to Dark later, do I need to choose "System" or should I choose "Dark"? Will this have unexpected effects on my whole computer if I choose "System" in this webpage?
> including a button that doesn't always do the same thing when pressed
The non-engineer would say the "System" one "doesn't always do the same thing when pressed" and that the "Light" and "Dark" in the 2-way control absolutely always do the same (and desired) thing: Immediately change it to Light or Dark. The side-effect of saving it as an override is, to be fair, a guess at their intent, but it's a very good bet.
Wikipedia (FWIW) says that the fictional USS Enterprise (NCC-1701) was named after the aircraft carrier USS Enterprise (CV-6) rather than the Space Shuttle Enterprise (OV-101).
GP is referring to in-universe canon, where the NCC-1701 was conceived and constructed by Starfleet, long after the Space Shuttle program was obsolete.
Wikipedia articles are largely discouraged from using in-universe perspectives or content, as opposed to Fandom/Wikia/Memory Alpha.
I'm not a DBA or sysadmin, but naïvely I feel like there's a difference between adding it to the client prompt and adding it to the server log. One-time startup messages in prompts/REPLs/etc. are noise (most of the time) anyway, but I feel like I'd expect logs to only contain things actually relevant to the operation of the software. Curious if anyone else feels this way.
I've never really understood this argument. If someone's a manager of an incompetent team, no amount of management skill will save the quality of the resulting software. I don't think "just treat LLMs like smart junior developers" fixes this, because well-functioning teams usually also have senior developers to keep things on track. Like, if we handed a team of genius-but-junior developers to the best "people person" manager in the world (i.e. who doesn't actually read the code), would we really expect decent results? Even if the manager tested the code by hand? I honestly don't think so, at least once the software gets past a certain (fairly low) threshold of size/complexity.
If you have a "this is an incompetent team" attitude, that's what quality software you'll get back; whether or not there's LLM use.
If you have a "I trust my competent team to write good enough tests and test coverage isn't my responsibility" attitude, that's what quality software you'll get back.
There are people producing good and excellent quality software with LLMs. Presumably you must discard low-quality code in order to maintain quality.
There's certainly a limit to code quality with current models. On number of lines of code per unit of time, LLM tools certainly already win.
Can costly automated code review for PRs catch most of the problems before they're under consideration for merge?
For example,
the vscode repo has extensive copilot integration. Every PR gets auto code reviewed. But with their tokens or the contributors'?
If I take poor quality code (AI-assisted or not) and spend a few hundred dollars on tokens for a next gen model and agent to get to 100% coverage and review for security bugs and CWE common weaknesses, what quality code will I have without refactoring with proven patterns and type annotations and polishing docstrings?
I don't think this argument holds. The OP made the very good point that most quality software teams are composed of both seniors and juniors, with the seniors (and even staff members sometimes) drawing the lines so that the system stays on rails.
If you're a manager now and your "team" is a bunch of coding agents, those agents are hardly junior engineers at best. It is equivalent or even worse than hiring a team of 3-5 junior engineers and letting them run rampant with your code.
> If you have a "I trust my competent team to write good enough tests and test coverage isn't my responsibility" attitude, that's what quality software you'll get back.
As much as this sentiment is nice, it is completely divorced from reality, unless the competence is verifiably there. If you take a bunch of juniors and say "yeah I trust them to do everything well enough," you're going to have a disaster on your hands.
The general sense of “liking” something is usually 好き (suki) in Japanese, AFAIK. Depending on the context (romantic, etc.), “love” could be 愛, 恋愛, 大好き, and probably others.
I ran into that issue too w/ sentence-based flashcards, where I almost immediately memorize the sentence itself and the whole thing becomes self-defeating. Similarly, I thought to use LLMs to generate fresh sentences on-the-fly, but the output was never reliable enough for my use-case... e.g. I came across some grammatical construction that the LLMs refused to use correctly. But, this probably depends on the language in question, since it sounds like you had success with it! Maybe I should try again at some point, now that the consumer models are a lot beefier than they were even six months ago.
I used it for practice Spanish. LLMs have no issues with generating decent sentences in it. Also as I practiced vocabulary building, I didn't need specific grammar constructs or even to be very sensitive to the occasional mistakes in this area (which I don't remember to notice).
It took me quite a bit of iterations to get AI to generate output I found good enough and with acceptable errors rate for my practice but that was the part of fun.
If anybody wants to try the same route, the biggest mistake not to repeat is to trust LLMs to generate words definitions by them itself. It does it quite well, but still gives wrong definitions from time to time (~1% in my case for the OpenAI models 2 years ago). This wasn't acceptable to me and took a lot of effort to review and correct cards I already had. Feed vocabulary article with word definition to LLM instead if you want it to generate word definitions suitable to your level instead.
I spent a few weeks in the cave and it was surprisingly chill, not nearly as oppressive as it sounds. (Although, I was much more energetic a decade ago and maybe it wouldn't be quite as fun these days :-P.) I still have a picture of my madness-induced, Git hook–infested scribblings....
[0] The team's usual room was an open floor plan, which was fine with good headphones, but naturally that solution doesn't work for pair programming.
reply