My chairman, Samir Khuller, asked me to post our job posting for a lecturer to my blog, so I and doing it right now. I think he overestimates the power of this blog.

At Univ of MD at College Park lecturers teach most sections of our intro sequence (CS1, CS2, CS3, Discrete Math). They might sometimes do a higher level course if the need arises. They are there to mostly teach and advise students, not do research, though some do and that's certainly fine. Some have PhD's and some don't. Note that this is a full time job--- these are not adjuncts or rent-a-profs. They are part of the department.

Is having lecturers teach the intro courses a good idea? Overall YES; however, I would like to have professors teaching those courses once in a while, or be involved once in a while, as they may have a good idea to share with the lecturer (then again, they might not). Having said that, you don't see me volunteering for CS1, CS2, or CS3 (My policy: I never teach a course where I would get a B if I took it. One exception- I did once teach Graduate Algorithms and got in a bit over my head.) I do teach Discrete Math once in a while. I also like to proofread the midterm and final of whoever is teaching it. I'm NOT that good a proofreader, but I like to know what they are up to and it gives me an excuse to talk to them about the course and make sure it doesn't drift to much. I would like to think I have a good rapport with the lecturers.

Does having a PhD in CS and being a professor give one some insights on what should be in CS1,2,3 and how to teach it? I honestly don't know. My first semester at Univ of MD (1985) we were teaching program verification in CS1. I knew immediately it was a bad idea and eventually (without any input from me) the dept stopped doing that. This is a case where being a researcher may be a negative with regard to education.

I would like to think that my working in theory helps me teach Discrete Math. It does as a source of some problems (e.g, if a paper says `by an easy induction...' that can be a problem set) but one should not get to carried away and go over their heads.

Dear Prof Gasarch,

ReplyDeleteI was very intrigued by your comment that its a bad idea to teach program verification in an early/introductory CS class. Could you expand on some of the negatives of doing this? I am a freshman taking an intro to verification class and wondering why.

--freshman

Here are my reasons. Others may differ and I welcome an intelligent debate.

ReplyDelete1) Intro programming should be FUN. Actually DO SOMETHING interesting with programming. Program Verification gets in the way of that.

2) To do program verification you have to have some math maturity and certainly be comfortable with induction. (Contrary to what some profs have told me, NOT students

DO NOT learn induction in high school.) If an intro to discrete math is a prereq to the course then that might work, but I am still skeptical.

3) I ask this nonrhetorically--- does learning program verification actually make you a better and/or more careful programmer? I wonder if proving programs correct rather than testing them and using intuitive reasoning is a mistake.

4) Debugging tools and testing would seem to be a better thing to teach, though that also may be better in later courses.

Dear Prof Gasarch,

ReplyDeleteThank you for your detailed and considered email. I agree with you and here are some additional points that I feel as I am being made to take this course:

1. we are taught verification in scheme which is a toy language, because we are told java/python has "state" which is hard to prove things about

2. we are taught using this tool acl2 which is a truly obscene tool, it will prove A=B but fail at proving B=A and weird things like this, I believe coq and isabel etc are not much better

3.#2 is explained away saying that anyway proving (even termination) is undecidable and so it is an art

4. we are taught little stylized schema for proving toy programs correct

5. the induction is actually the fun part of the course and so are the proofs and instead of explaining how the rewrite rules (of inference) are a way of confirming intuition, all the intuition gets beat out of us by making us do these stylized syntactic transformations the way it is coded in the acl2 tool, we are never taught to build/drag a model alongside our proofs

6. no attempt is made to explain the larger landscape of models and theories and the various cool theorems like completeness/incompleteness, upward lowenheim-skolem (nonstandard models) and connections to undecidability; in fact when I ask the teachers they themselves understand very poorly the connection between computability and completeness, some don't even appreciate that incompleteness is not the opposite of completeness - how do they expect to teach verification with such limited understanding.

All in all it feels like (a lot of) Programming Languages and Formal Verification theory is a profession run amok that wants to justify its existence by cramming meaningless stuff down the throat of freshmen.

--f

Program verification can be a useful thing to learn when you already have some programming experience. You are probably never going to do any formal verification after the course, but your approach to programming may become more structured and rigorous. Loop invariant is pretty much the only concept I still remember from my program verification classes, but it's so useful concept that it alone justifies taking the course.

ReplyDeleteBill,

ReplyDeleteWe have several different intro programming tracks at Chicago, and different staffing strategies for each.

A senior faculty member teaches the honors track (that's been me for quite a while at this point). The main track (suitable for CS majors) is taught in multiple sections, a couple of which are taught by a senior lecturer, and at least one is taught by a faculty member. We also have a course intended for scientifically oriented non-majors which is taught by senior faculty. Finally, there's a programming for non-scientists course which is taught exclusively by senior lecturers. If it weren't for the fact that one of those lecturers had a prior existence as a CS prof at a major university, I'd worry about it. As is, I don't.

BTW, my Honors programming I class is taught in Haskell. I'm not sure I'd recommend this for a general introductory course, as much a fan as I am of functional languages and expressive type systems. But for my students, it's worked out very well.

As for verification -- it is different in functional languages. I definitely encourage my students to think rigorously about the code they right, but I'm skeptical about attempts to hammer rigorous thinking about code into a single formal paradigm (e.g., Hoare triples). Programs are proofs, after all, and proofs are infinitely varied.