Formal Methods of Software Design: an online course by Eric Hehner | Hacker News Reader

Formal Methods of Software Design: an online course by Eric Hehner

cs.toronto.edu

81 pointsbumbledraven8 comments

I learned CS his way (my alma mater is where Edsger Dijkstra laid his eggs). It's a very nice way of thinking, and certainly worth your time. Warmly recommended if you know programming but not formal methods.

That said, I wish courses like this would stop using terms like "software design" or "software construction" in their descriptions. This course hardly seems to step out of the realm of algorithms.

This has absolutely nothing to do with software design, unless your program has 300 LOC in total. Software design is much more a social science than most CS researchers dare to admit, so they just keep refining their techniques of dealing with advanced but finegrained things that few programmers do a lot (such as algorithms).

From what I see on the front page, the course seems to be based on the notion of refinement, i.e. transforming a high-level specification into a concrete implementation by refining the specification in several steps. There is a recent example [1] of a software development process based on refinement. The authors build a fully verified model-checker using Isabelle/HOL. The code has a non-trivial size (4900 lines of ML) and implements complex functionality (model-checking algorithms) in an efficient way. Roughly speaking, it is proved that the model-checker reports the violation of a property if and only if the system under scrutiny does violate the property.

[1] http://cava.in.tum.de/templates/publications/CAV2013.pdf

Any modern course on formal methods in software design should at least mention modern tools like coq, however, in this course there're no mention of them.

Hmm, that is unfortunate. However, since my university recently canceled its only class that covered formal methods in any depth, I haven't been able to find any great options for learning about this area in a structured way. Perhaps you could provide an alternate, superior option?

If you want to get started with Coq there are two good resources. One is Software Foundations[sf] by Benjamin Pierce. There's also Certified Programming with Dependent Types[cpdt] by Adam Chlipala. I would say [cpdt] is more advanced than [sf], so I think it's best to start with [sf] and then start on [cpdt] if you feel up for the challenge.

I have mixed feelings about Coq as a tool for software design. On the one hand I think it's feasible to use Coq to prove correctness properties of your programs. On the other hand I feel it can sometimes be extremely tedious and / or difficult to show some properties. I do believe it is the future to prove properties about parts of your program, though.

Lately I have been working on brainfuck in Coq[bf] in my spare time. I have spent almost two weeks on the project now and I have been able to show that 1) the "Hello World!" program on brainfuck's wikipedia page does indeed output "Hello World!"[hello], and 2) the correctness of a simple compiler from arithmetic expressions (with +, -, and *) to brainfuck[compiler]. The project is more than 1000 lines of code. I must admit some of the code / proofs are messy and could probably be shorter, but I think it does indicate how much work it requires (and how messy brainfuck is!)

[sf]: http://www.cis.upenn.edu/~bcpierce/sf/

[cpdt]: http://adam.chlipala.net/cpdt/

[bf]: https://github.com/reynir/Brainfuck

[hello]: https://github.com/reynir/Brainfuck/blob/master/bf_theorems....

[compiler]: https://github.com/reynir/Brainfuck/blob/master/ae_compiler....

Edit: I just remembered this talk by Wouter Swierstra where he proves some correctness properties for the core of xmonad: http://www.youtube.com/watch?v=jqaOU8kqykg (unfortunately I can't find the slides at the moment).

have you any experience with alloy? http://alloy.mit.edu/alloy/ - that seems like it's aiming for a middle-ground somewhere between coq and crossing your fingers.

Coq is an excellent tool for software-assisted theorem proving, but it can also be good to know how to do certain things without the help of a computer. This course is about a theory of programming that's practical and simple enough to use on its own, without support from a tool like Coq, just like one might calculate the answer to a multiplication problem on pencil & paper, without using a calculator.

For all its simplicity, the theory is still general: it deals with parallel, sequential, probabilistic, deterministic, standalone, and interactive programs, as well as time (incl. real-time) and space bounds. It can even be used as a rigorous way to solve probability problems by hand, by writing a program to simulate the scenario and proving what its result is. (http://www.cs.toronto.edu/~hehner/ProPer.pdf)

I feel pretty out of my league even commenting on this, but I'll do so anyway.

As someone who's gotten by quite well with thinking about boolean logic as just true and false, the first two videos have absolutely blown my mind.

Reply on news.ycombinator.com