Teaching programming and formal methods

Question

Here's a sort of odd question. I'm in the process of writing a book on learning to program using formal methods, and I'm going to target it toward people with some programming experience. The idea is to teach them to be high-quality programmers.

The basic notation is going to be from Dijkstra's Discipline of Programming, along with some concurrency and communications extensions.

Unlike EWD, I want my students eventually to write actual executable programs. That means at some point translating from EWD notation to some other language. When I first started doing formal programming I targeted C, but you end up writing a lot of plumbing, plus there are all the complexities of treating pointers etc. Ruby is an obvious possible target, as is Scheme or Lisp. But there are also the various function languages; since I'm especially interested in concurrency, Erlang seems like a possibility.

So, finally, here's my question: What language(s) should I teach my readers to target their formally-developed programs?

Answer 1

Hi Charlie

That's a nice idea. I think Scheme is a good option as it allows one to put into practice(in the form of libraries) different abstractions with a bare minimum essentials. It is also easy to translate from scheme to a verification system like PVS (http://pvs.csl.sri.com/)

cheers

Answer 2

I grew up on Lisp and Scheme and love them both. I think they are great languages to learn from scratch on. But, I'm not sure someone with some programming experience would take to those languages. You're not going to get a lot of hits on Amazon for your book with Scheme in the title. :)

C# is a very easy language to learn and it's got all the basics you would need to dive into topics like concurrency pretty quickly. It has more applicability because you can target OO and web concepts as well. It's also fairly popular and you would get companies paying for their employees books which is always good for sales ("Be a Kick Ass C# Programmer" goes much further on an expense reimbursement sheet than "Concurrency in Modern Lisp").

F# is an interesting language. It's got the functional beauty of a Lisp or Scheme (well not quite, but almost) and it gives you some ability to dive into OOP topics as well as hook into the .NET Framework for UI stuff if you want to spice things up. But, right now, it's obscure.

I can't speak to Ruby, so personally, I would bite the bullet and go with C#.

Answer 3

I think that you should yourself have quite some experience in the language you use for your book, or someone proficient to review your code.

Personally, I'd use Common Lisp, since I am familiar with that, and it's a great language to implement any concept. Other options might be Erlang, Haskell, Ruby, or Python, perhaps even some ML dialect. I am biased against the C family (including C# and Java), they seem stuck to a lower level of thinking about concepts.

Answer 4

Ignoring the obvious what's your favorite programming language answers, I can see two useful answers:

On the one hand, you are trying to demonstrate methods to what are presumed to be intermediate programmers. If you select a single language and bless it as your books language, you will possibly alienate potential readers that don't happen to prefer that language for one reason or another. Since you're demonstrating methods, You have the luxury of using snippets in languages that happen to illustrate your point concisely. For example, the only language available for demonstrating RIIA is probably C++, but this same language is pretty poor for showing how to perform source analysis. Scheme is ideal for source analysis, but doesn't give you very many options for exploring the benefits (and weaknesses) of strong typing. Use many languages.

On the other hand, since you're mainly up to methods of programming, I'm not totally sure you need any real language at all. A well defined notation is just as good, and forces your readers to focus on the point you're making rather than the superficial details of one language or another.

Answer 5

Charlie,

I have always associated Dijkstra's masterpiece with a model of programming in which center stage is occupied by loops and arrays. If you're sticking close to Dijkstra (e.g., computing weakest preconditions) I think you'll find functional languages are not a great fit. Of the popular languages that provide good support for imperative programming with loops and arrays, perhaps Python carries the least additional baggage.

This is not to say that functional languages are unsuited to formal methods---they are very well suited---but the style is quite different from Dijkstra. The preferred methods emphasize calculational proofs; see Richard Bird's paper on solving Sudoku (which is heavy going) or the textbook by Richard Bird and Phil Wadler.

For concurrency it depends a lot on what model of concurrency (and what formal methods) you believe in. John Reppy's Concurrent ML is a beautiful message-passing model. Erlang also has a nice clean restrictive model. On the other hand, programming with locks and critical sections is so difficult, there may be more benefit to formal methods in that situation.

Two other passing remarks that may be of interest for your background research:

• The only programmer I ever met who applied Dijkstra's methods in practice to real systems was Greg Nelson, who was working in Modula-3. (Greg and Mark Manasse wrote the Trestle window system together.) Modula-3 was a very nice language that Digital allowed to die through fecklessness and incompetence. Greg had a nice TOPLAS paper on an extension to Dijkstra's calculus.

• Gerard Holzmann's modeling language SPIN is based directly on Dijkstra's language of guarded commands, and it also supports concurrency. Its purpose is model checking, not programming, and there are a few idiosyncracies, but there is a strong connection with formal methods, and it's really great to be able to model check your assertions. Anyone interested in formal methods will want to check it out.

(Edit: Here's a link to the Greg Nelson paper, or one of them. — CRM)

Answer 6

Honestly, I can't recommend Ruby for this. When I program day-to-day in my commercial world, I like it quite a lot, certainly much more than C or Java. But the semantics of it are so ill-defined that I don't trust it half as much as C where, though I may spend several hours arguing over a statement and consulting that much thicker white book that replaced K&R, I come out in the end fairly convinced that if I've got a conforming compiler (yes, I know, I'm a dreamer, but work with me here) I know what's coming out the other side.

Ruby is wonderful in many ways, but as far as anything formal goes, the twain will never meet.

I'd tend to vote for Haskell myself, because every time I turn around I'm amazed at how much sense everything makes in that language definition. (Though admittedly after only a year or so at it, I'm sure I've not explored half the corners of even Haskell 98.)

And I understand, too, the Dikjstra vs. functional thing; going back and reading his papers he's very much in an imperative world; I am not qualified to say whether he really went the wrong way there. Perhaps I'm just overwhelmed by how good his writing is, as much as his thought. But it did seem to please him, so what about using Algol 60?