Home

Johannes Åman Pohjola [2023-05-27 Sat 18:09]

If you are enrolled in the course as of this announcement, you should either be already enrolled on the Ed Forum, or you should have received an invite in your UNSW inbox. If you have not, check your spam filter. If it's not in your spam filter there, try logging into Ed with your z<digits>@unsw.edu.au address—Ed doesn't have the best track record with UNSW email aliases, so chances are you have more than one account. If that doesn't work either, send us an email to cs3141@cse.unsw.edu.au as soon as possible and we can get it sorted.

The Ed forum will be the primary venue for discussion and announcements throughout the course. I strongly recommend checking it regularly.

Johannes Åman Pohjola [2023-05-16 Tue 19:00]

Hi, I'm Johannes and I will be the convenor and lecturer-in-charge of COMP3141 this year. Scott Buckley will do practical lectures, and Tsun Wang "Gordon" Sau and Rahul Tripathi will help out with course administration, forum and assignments.

This course has previously been taught by many others, from whom I inherit the bulk of the material. This includes (in no particular order) Gabriele Keller, Liam O'Connor-Davis, Christine Rizkallah, Curtis Millar, Raphael Douglas Giles and Zoltan A. Kocsis.

More stuff will pop up here within the next few weeks. In the meantime, here is Zoltan's excellent description of what the course is about from last year:

COMP3141 has a very vague course title, so many of you may be curious as to what this course is actually about, and what it involves. You may have heard that COMP3141 is a "Haskell course". In reality, it is a software engineering course that happens to use Haskell.

Here, software engineering does not refer to the mixture of project management techniques and object-oriented programming. Rather, we mean mathematically structured programming: rigorous software engineering using sound mathematical principles.

The course will cover a variety of programming techniques that make use of semi-formal and formal methods for the design and implementation of real-world software systems. It introduces approaches to testing informed by formal designs, and it covers trade-offs between static and dynamic approaches to improving software correctness.

Some of you may have learnt (or will go on to learn) about formal verification from other UNSW courses such as COMP4161. While this is an admirable pursuit, this course is not about formal verification either. Rather, we investigate the use of mathematically structured programming to deliver software that is more reliable, more verifiable, and more elegant.

Central to the notion of mathematically structured programming is the art of specification. Writing formal specifications and understanding their limitations is a central theme of this course. In the course, we will learn how to translate these specifications into meaningful artefacts that relate to a Haskell implementation, such as logical property-based tests, type-system enforced invariants, or proofs via equational reasoning. We will investigate design patterns based on mathematical ideas, and ways of thinking compositionally to produce working software in a bottom-up fashion.