3
$\begingroup$

I have been told to teach a Functional Programming and Verification course that specifies the following topics:

  • Correctness of imperative programs
    • Verification according to Floyd or Hoare
    • Termination
    • Procedures
  • Basic concepts of functional programming
    • Values, variables, functions
    • Data structures, pattern matching
    • Higher order functions
    • Polymorphic types
    • Programming in the large: Structures and Functors
    • Correctness of functional programs
      • Semantics of functional programs
      • Verification of functional programs
How can I teach Functional Programming and Verification?

And in particular:

  • Which programming language should I use for programming assignments?
  • Are there any suggested tools and resources?

The only course I have found online is: Functional Programming and Verification

Improve this question
$\endgroup$
2
  • $\begingroup$ How versed are you in FP and the topics listed? $\endgroup$ Commented Nov 15, 2024 at 14:07
  • 1
    $\begingroup$ I am not that versed/experienced in them :-( But I have 3 months to study. $\endgroup$ Commented Nov 15, 2024 at 14:30

4 Answers 4

Reset to default
3
+100
$\begingroup$

In what seems like a past life, I taught functional programming as part of a Programming Languages course. Most of the students had no exposure to functional programming but did have experience in languages like C++ or Java. Those language have a very different underlying mental model, but use lots of syntax. I thought it a mistake to drop both of those (mental model, concrete syntax) for a new language so chose Standard ML as the language, as it has the right mental model, but uses concrete syntax to help guide the user and reader. Lisp and its immediate variants use only abstract syntax (basically nested parentheses and indentation) in place of concrete syntax.

Modern functional programming languages that use concrete syntax are the ML variants, including OCaML, as well as Haskell, and Clojure. I'd suggest that you explore each of those, rather than LISP itself.

As a personal note, I found that I could program quite effectively in ML, but remain very unskilled in LISP.

You could, of course, also, teach in one of the more modern functional programming languages and periodically show how the same things are expressed in LISP with only abstract syntax. There is a close overlap in the concepts.

I have a friend who was a student of McCarthy (inventor of LISP) and who, himself, did some important work with the language and its libraries. He once told me that he could look at a LISP program and its indentation structure and know, pretty much, what it did. I was skeptical, but he was good enough generally to be believed when he said such things. I never got close to that level.

Improve this answer
$\endgroup$
3
$\begingroup$

This is not an area where my expertise runs deep, but it seems to me that you want a functional language that supports types, and also works well for program verification. On that basis alone, I'd steer clear of LISP/Scheme, as it does you no favors when studying types. My understanding is that OCaml and Haskell both have strong type systems, and also work well for program verification, so I would steer strongly towards something of that ilk.

Given the focus on functors as well, I might head to OCaml, since my understanding is that it makes functors more obvious and explicit than Haskell.

Again, I am no authority on this topic, but OCaml seems like a strong starting point to me for your learning goals.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Thank you. Please note that I have been informed students are particularly interested in learning LISP. $\endgroup$ Commented Nov 18, 2024 at 12:00
  • 1
    $\begingroup$ @alper They may be interested, but I'd avoid it given the rest of that curriculum list. I suspect they'd have a fair amount of difficulty with those concepts in that language. $\endgroup$ Commented Nov 19, 2024 at 21:00
2
$\begingroup$

I took the following two courses when I was studying for an MSc in Software Engineering many years ago:

  • Advanced Functional Programming
  • Formal Basis for Computation

These were courses given to BSc Computer Science students at the same time (who had studied these subjects earlier in their studies).

The book we used for Advanced Functional Programming was Elements of Functional Programming by Chris Reade (who was our lecturer for both courses). We also used Standard ML as the programming language for examples and coursework and I do remember our lecturer not being very keen on using LISP (assuming my memory is serving me well), so I can confirm the information given in another answer to your question.

I cannot remember much about the Formal Basis for Computation course, but I do remember it was about Formal Methods and Z, however, I can no longer remember the book the course was based on.

Each course was based on their respective books and we really needed to learn no more than what was contained in the books.

I had a background in C++, Assembly Language, BASIC, and FORTRAN so these courses showed me a different way of thinking about programming.

Improve this answer
$\endgroup$
2
$\begingroup$

There is NYU's Edward Z. Yang's PL Class which teaches basics of functional programming with a little bit of introduction of lambda calculus as well. This made me love Haskell.

For formal verification, I suggest using Software Foundations. It is a great resource if you are willing to put the effort.

If you don't want to start with Haskell, I suggest using something LISPy like the book Structure and Interpretation of Computer Programs or The Little Schemer Series of books.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.