CS 2102

Kevin Sullivan definitely knows the language he's trying to teach and understands the logic he's trying to teach, but is not that good at teaching itself. Lean is also still a pretty experimental coding language, so you can't look online for answers. I highly recommend making a solid friend group in this class so you can all figure out the concepts together, because you don't want to waste your time going to office hours. The TA's were also pretty confused (might be different next semester) and Sullivan's OH are always busy because.. well, nobody knows what they're doing. He does assign homework but he never announces it in class so you have to start working on it as soon as he posts it on Collab (unexpectedly). In class, he spends such a long time going over the same concept and the same problems, but doesn't thoroughly explain the harder concepts. Not a bad course because you feel so accomplished when you're done AND Sullivan is an easy grader, but I definitely didn't learn much. Solved every problem on the final exam but not really sure what each command does (thank god for open note!). Honestly, don't take this unless you need it for CS or you need a grade booster.

The hardest part about this class was staying awake. Sullivan is a great lecturer but the content was mostly boring, or taught too slowly to be interesting. It used to be a logic class with writing by hand, but now it's about coding in lean and it's not run well enough to be useful. I'd only take this if you have to for your major, but even then you can get out of it by taking the discrete math class in the math department (at least if you're going for a BA in CS), and that's a lot better.

This course is awful. Sullivan is nice, but can't teach to save his life. Exams have problems with concepts that were never taught. One homework I struggled on for a long time, only to come into class the day AFTER it was due and have Sullivan teach how to do the exact problems I was struggling with. How am I supposed to know how to do the problems if he hasn't taught them yet??? Extremely frustrating.

~TLDR: If you can possibly take this class somewhere besides UVA, do it. Sullivan is probably the worst professor I've ever had. He's kinda nice, but also isn't accessible and doesn't even know the material that well. ~

This is without a doubt the worst class I have ever taken. I thought that intro to engineering lab with Ann Reimers was the worst class I'd ever take but I was wrong. I at least used the information that I learned in Reimer's class, and I can't see that I will ever use this information ever again.

I came into this class excited to learn discrete math and was instead given a cheapo version of discrete in a theorem prover where the only reliable proof technique we learned was to throw commands at the theorem prover and hoping something would work. Here are some of my biggest issues with the class:
- Sullivan just used shorthand tactics while teaching instead of explaining the actual logic.
- The textbook was overly verbose and ultimately unhelpful.
- Exams frequently had material that was far harder than problems in the homework, lecture, or notes.
- Sullivan didn't hold office hours while the homework assignments were open. He posts the homework on Thursday, it’s due on Tuesday, and his office hours are on Wednesday.
- Sullivan never responds to emails.
- Sullivan doesn’t actually know lean very well, and his assignments are full of syntax errors which make it impossible to prove the theorem as written.
- Sullivan often showed up to class unprepared to teach and just made up exercises as he went which was evident by the fact that he continuously messed them up

I found this course to be extraordinarily easy, to the point where it was far too slow-moving. Sullivan teaches you all the tactics you need in lean, a fairly strange automated theorem prover that replaces the pen-and-paper aspect of this course. While I don't think you learn the logic as well as you might in a traditional discrete math course, I think lean is an interesting concept and teaches functional programming in addition to logic fairly well. The only major problem with this course is that a good amount of it has to come from self-study, which is okay as long as you find the material interesting. Sullivan commonly spends lectures showing videos of rocket crashes and telling his students that this is what can happen if your software is no good, rather than progressing the course further, making it very slow at times, since we spend more than a week on proving one type of proposition. We also never made it to sets or automata, which was disappointing, but overall one of the easier classes I've taken at UVA.

Honestly, If you asked me if I learned a single thing this semester, I would say no except for how to struggle with writing proofs in lean. Sullivan is an ok professor and a very nice guy but I haven't learned anything other than how to fuck with Lean in order to try and make it work. The work is fairly easy except no one has any clue what is going on and even the TA's are confused on how to do things sometimes. I never needed to learn anything other than how to do proofs in lean, not how they work or why just that I can solve it in lean. Furthermore, a lot of the time they would give us assignments that had information we had not learned or had to use some obscure tactic in Lean in order to solve it. And this language is so obscure that when you look up "how to use and.intro in lean" it will give you results on how to drink lean......, I feel woefully underprepared going into algo and Theory.

This class is extremely disorganized. The homework and test difficulties range from stupidly easy to ridiculously impossible. The lectures make little to no sense and sometimes he would use a tactic and never explain what it does or why he used it there. We had like 6 homeworks on the first 6-7 sections, and then like 2 on the next 12. Lectures would consistently introduce topics that we had needed for the homework that was due the night before. We didn't know the location of our final until the day before. Even the TAs were sometimes clueless as to what's going on. I doubt anyone who has ever taken this class has ever even touched Lean (the language we use to code) afterward. I could go on and on but you get the picture

We don't learn much, but it's an easy class. But it's also easy to get totally lost and thrown off bc we use LEAN. Just take it since it's a requirement!

I think the best way to describe this course and this professor is "Oh no." He is beyond disorganized and the lectures make next to no sense. This course is problematic to say the least. If possible try to take it during the summer instead because they don't use LEAN at all! Prof. Sullivan is a really nice guy and worked to accommodate for people's schedules and such, but he is like the Rising Roll of professors (that's to say that he is a hot mess). Exams are open notes and there are reviews but nothing gets graded quickly so there is very, very little feedback on your work. If you take this class, I wish you good luck...you'll need it :)

Sullivan is brilliant, definitely talk to him personally if you are having any issues. While he is somewhat disorganized, he teaches discreet in a much better fashion than the traditional, writing proofs with pen and paper. You are learning while the curriculum and coding languages involved are still in development - so keep that in mind. He offered many opportunities for extra credit as well. Honestly the whole class was easy if you followed along in lectures, otherwise you could catch up with his self-published materials which he offered for free.