Georg WeissenbacherMar 5
@krismicinski @shriramk @jfdm @csgordon @lindsey @jeremysiek we have been claiming for decades that we are not just educating coding monkeys, so it shouldn't really matter that LLMs can now do all the coding. As far as I see it, it's still necessary to identify and clearly formulate verifiable requirements and specifications, come up with a modular design, and verify the whole thing, because I still believe the ultimate responsibilty lies with the developer. So students still need to understand the fundamentals. But yes, it has become much harder to check *at scale* whether they actually grasped them.
Show threadShriram KrishnamurthiMar 6

@GeorgWeissenbacher @[email protected] @jfdm @csgordon @lindsey @jeremysiek
Yes to most of that. I think it's not that hard to assess if that is what people were always assessing that.

I actually disagree w/ your opening comment. Most intro CS educators will say (and have said), "I don't teach programming, I teach *problem solving*" (whatever the fuck that is). My response is, "great, this should be your liberation! Programming got easy, what are your «problem solving» ideas?"

Show threadTony Garnock-JonesMar 6
@shriramk @GeorgWeissenbacher @krismicinski @jfdm @csgordon @lindsey @jeremysiek ... did programming get easy? Can one be said to be programming if one asks someone else (or an LLM) to write a program for you? Or is some other kind of (not- or not-quite-programming) interaction going on?
Show threadShriram KrishnamurthiMar 6
@tonyg @GeorgWeissenbacher @[email protected] @jfdm @csgordon @lindsey @jeremysiek
I very much think of what I'm doing with Claude Code as a kind of programming — indeed, the kind of programming I always wished I could do! But if it makes you happier to use a different term for it (not "vibecoding", that has too many specific connotations and is definitely not how *I'm* doing things), and it's *useful* to have that other term…that's fine by me. I guess my slogan is: "Philosophy…but not too much".
Show threadLindsey KuperMar 6
@shriramk @tonyg @GeorgWeissenbacher @krismicinski @jfdm @csgordon @jeremysiek This comment made me realize something about myself: this is *not* a kind of programming I always wished I could do. I really only like programming because I like manipulating formal systems. That might explain a lot about why this kind of programming doesn't appeal to me, aside from all the bad externalities.
Show threadShriram KrishnamurthiMar 6
@lindsey @tonyg @GeorgWeissenbacher @[email protected] @jfdm @csgordon @jeremysiek
You were formal about some things and utterly informal about other things. Where, for instance, did you document your software architecture, your temporal properties, your concurrency requirements, etc.? I'm going to guess a whole bunch of things were *not* captured by your "formal systems" and were left to documentation, comments, hopes, dreams, and aspirations. ↵
Show threadckfiniteMar 6

@shriramk To me this is an odd (and, frankly, extremely personal-seeming) attack. It is possible to have a formal system that one enjoys manipulating (a subjective assessment) that is limited in scope or does not capture other aspects of the system. I, fundamentally, do not think that you must formalize your entire world in order to pick parts of it off into interesting and fun abstractions that can be manipulated into and of themselves.

I read this as arguing that Lindsey's personal, subjective, enjoyment was invalid due to not having a complete formal world model, and I ultimately think that this isn't a valid position. You might not have the same opinion, but I find it bizarre to argue that the very enjoyment is wrong.

Show threadShriram KrishnamurthiMar 6
@ckfinite Nowhere did I question Lindsey's right to, or sense of, *enjoyment*. Nor would it make any *sense* for me to say "no, you didn't really enjoy the thing you said you enjoyed". I'm pointing out that Lindsey was already informal in various ways, and PL people have a particular blind spot about how formal/informal we really are (as in, we think we're super-formal when we're actually only 1-2 degrees more formal than the entirely-informal).
Show threadckfinite

@shriramk To me, I read quite a lot of the terminology you're using as being very specifically judgemental, and when combined with the second person framing it becomes very personal.

When contextualized with a statement about a subjective position, about a personal feeling, it comes off as either:

* A value judgement of the feeling that she's expressing in and of itself; that it is wrong to feel enjoyment from a partial formalism and that your viewpoint is categorically better, or
* A category error where you're making a point about the community come off as a judgement about a person.

I agree with your point about the community, but think that the way that this is framed is coming off very strongly as the former where your response to me was that you were intending the latter.

> as in, we think we're super-formal when we're actually only 1-2 degrees more formal than the entirely-informal

I would contrast this answer with what you said earlier

> To be fair, I too suffered from this flaw until Gregor Kiczales kindly beat it out of me with a few pointed remarks.

to imply that no, you are different, you are entirely formal because you are disclaiming yourself of the flaw.

I'm not different; I'm very informal. These days I work mostly in physical simulation and embedded control systems, and there's tons of informality in both settings. What I think that those domains illustrate, though, is that even for a "fully formal" software system, where the architecture, the temporal properties, the concurrency requirements are all fully specified large parts of the system aren't and go quietly unnoticed.

A classic example is Therac-25, where the race condition was between the speed the user typed at, the UI state, and the speed the machine's turntable rotated at. A more modern example would be rowhammer. Even in systems where everything's formally verified and proven down to RTL you still have informality in the analog domain.

Mar 7 at 12:30amWeb
Show threadShriram KrishnamurthiMar 7

@ckfinite Thanks for this critique. I definitely did not mean to make this *personally* about @lindsey . Since I have given that impression — sorry, Lindsey. I always think of Lindsey as one of the "good eggs", so I *especially* don't mean to call her out personally.

I do mean to call out the PL community broadly, though. And I say this as someone acknowledging my own flaws in this regard. I'm not sure how you read my Gregor comment as me saying I am "entirely formal", but probably no matter.

Show threadLindsey KuperMar 7
@shriramk @ckfinite I did think your comment was a weird non sequitur, Shriram. I made an observation about myself and what I like about programming, and you responded to that with a broad critique of the entire PL community, with me as a proxy for it. I'm not even sure that what I said is even really an example of the community-wide tendency that you're critiquing. It seems more like you had something queued up to say and I accidentally pushed the particular button that made it come out.
Show threadShriram KrishnamurthiMar 7
@lindsey @ckfinite
Probably. I'm sorry, again.