tag:blogger.com,1999:blog-3722233.post1315264733447474170..comments2021-11-26T15:18:15.242-06:00Comments on Computational Complexity: Maryland looking for a Lecturer/Who teachers your intro courses?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-3722233.post-77035240581839187642014-02-18T12:59:39.923-06:002014-02-18T12:59:39.923-06:00Bill,
We have several different intro programming...Bill,<br /><br />We have several different intro programming tracks at Chicago, and different staffing strategies for each.<br /><br />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.<br /><br />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.<br /><br />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.<br />stuhttps://www.blogger.com/profile/05190631846507740664noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-37947408296202160372014-02-17T19:48:29.361-06:002014-02-17T19:48:29.361-06:00Program verification can be a useful thing to lear...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.Jounihttps://www.blogger.com/profile/08868620962601644633noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-66276131643864876252014-02-17T16:41:59.395-06:002014-02-17T16:41:59.395-06:00Dear Prof Gasarch,
Tha...Dear Prof Gasarch,<br /> Thank 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:<br />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<br />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<br />3.#2 is explained away saying that anyway proving (even termination) is undecidable and so it is an art<br />4. we are taught little stylized schema for proving toy programs correct<br />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<br />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.<br /><br />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.<br /><br />--fAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-91116494686082963262014-02-17T11:23:18.147-06:002014-02-17T11:23:18.147-06:00Here are my reasons. Others may differ and I welco...Here are my reasons. Others may differ and I welcome an intelligent debate.<br />1) Intro programming should be FUN. Actually DO SOMETHING interesting with programming. Program Verification gets in the way of that.<br /><br />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<br />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.<br /><br />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. <br /><br />4) Debugging tools and testing would seem to be a better thing to teach, though that also may be better in later courses.GASARCHhttps://www.blogger.com/profile/06134382469361359081noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-49625436696269543432014-02-17T11:06:54.040-06:002014-02-17T11:06:54.040-06:00Dear Prof Gasarch,
I ...Dear Prof Gasarch,<br /> I 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.<br />--freshman Anonymousnoreply@blogger.com