Lambda the Ultimate

inactiveTopic Beseme Project Overview
started 11/22/2001; 3:53:47 AM - last post 11/24/2001; 8:47:21 AM
Ehud Lamm - Beseme Project Overview  blueArrow
11/22/2001; 3:53:47 AM (reads: 2348, responses: 10)
Beseme Project Overview
(seen on the Haskell mailing list)

Beseme is about teaching discrete math using functional programing (Haskell, to be exact). The basic idea is to teach CS1 topics in a more mathematical and rigorous way, mainly by introducing proofs and fomral definitions. Functional programming obviously helps, since it makes reasoning about programs so much easier.

This is closely related to some ideas I've been thinking about for some time now. To put it bluntly, after traditional CS1 courses it is a small wonder that some people actually manage to produce reliable software.

Visit the Beseme project home page.

Posted to teaching/learning by Ehud Lamm on 11/22/01; 3:54:37 AM

Noel Welsh - Re: Beseme Project Overview  blueArrow
11/22/2001; 5:53:19 AM (reads: 1637, responses: 0)
I really wonder if this sort of education will reduce bugs. Most bugs I've seen fall into two categories:

i) stupid mistakes that are easy to fix ii) misconceptions about the problem domain that are hard to fix

This sort of education won't address ii) which is where the real problems lie IMO. More flexible development methodologies (e.g. XP) and more flexible languages (e.g. [insert your favourite here]) will help.


Ehud Lamm - Re: Beseme Project Overview  blueArrow
11/22/2001; 6:56:20 AM (reads: 1643, responses: 1)
Not dismissing the categories you mention, I think we should aslo remember that there are also logical errors in algorithms (even when you copy them from books!). Even plain vanilla programming errors can be problematic to weed out if there are enough of them, and if the manifest themselves in subtle situations.

Think for example about the ill defined (or undefined) IO model in many languages. It is many times hard to tell, or simply easy toignore, what remains in the buffer after reading some data, and when exactly the EOF event is raised (after reading the EOF, after reading the last character of user data etc.)

The bugs arising from these problems are easy to fix. But consider the approach to programming they often result in: You code the program, see the bugs and then do some ad-hoc fixing. Each programmer has his own style of dealing with these issues, so reading code and being sure of its quality can be problematic. What's worse, you stop playing with the code when it seems to work. So you get used to starting with code you are unsure of, playing with the code - perhaps breaking some hidden assumptions - and stopping when you get tired or don't find any obvious bugs.

This is fine in many cases, and I have nothing against this approach to programming. But this is not the way to build provably relaible software. And more testing, yeras of SE experience shows, doesn't help much either.

Luke Gorrie - Re: Beseme Project Overview  blueArrow
11/22/2001; 8:39:52 AM (reads: 1617, responses: 1)
What're some examples of "reasoning about programs", and why FP is better for it? I hear the expression so often but don't know what people mean by it. I'd be glad if someone would show some practical examples with appeal to people who aren't programming language designers or compiler writers.

I'm aware of the basic referential transparency example, but want more :-)

Noel Welsh - Re: Beseme Project Overview  blueArrow
11/22/2001; 9:55:08 AM (reads: 1709, responses: 0)
I think program proofs are at their most useful when one is proving algorithm correctness (where by algorithms I mean the stuff you find in algorithm textbooks). I suspect this is because program proof techniques have developed hand in hand with algorithm design. I imagine they are less useful when dealing with properties such as "ensure the customer is charged the sales tax appropriate to their state".

I definitely agree that well defined languages (which you raise "the ill-defined IO many languages") are easier to program in, becuase they are easier to reason about. However that reasoning may be informal. Ie the programmer's mental model is simpler.

However, I disagree when say more testing doesn't help. For the last year of so I've been coding in an XP fashion which means testing upfront. I've found the quality of my code has vastly increased and the more tests I have the less likely it is there are remaining bugs. Maybe I'm just operating on high gain part of the slope and doing more testing won't help beyond a certain point by so far that isn't my experience.

Finally, you state "provably reliable software" which implies this is desirable. Unfortunately I've learned that bug-free software doesn't pay. There is always the tradeoff between time and quality and the point on that continuum that proven software occupies is seldom optimal. Unless proof techniques can get a heck of lot better than they currently are there isn't much value to them in day to day development.

Ehud Lamm - Re: Beseme Project Overview  blueArrow
11/22/2001; 1:39:11 PM (reads: 1614, responses: 0)
I like the ideas of XP, but I find many of the claims to be exaggerated. Testing is simply not enough. Read about why companies decide to invest in formal methods. Anyway, I think this debate by itself will not advance the industry.

I agree that many times informal reasoning is enough, and I am all for languages that are clean enough to make such reasoning easy.

I agree that in most day to day programming situations proving correctness isn't cost effective. My guess is that this can be helped by having better languages and tools.

Ehud Lamm - Re: Beseme Project Overview  blueArrow
11/22/2001; 2:37:26 PM (reads: 1594, responses: 0)
An example of why testing isn't good enough? Think about security. The OS is tested, and is deemed secure until some hacker finds a chain of events that leads to a security problem.

Michael Christopher Vanier - Re: Beseme Project Overview  blueArrow
11/22/2001; 6:45:10 PM (reads: 1603, responses: 0)
This is really fascinating -- using Haskell to teach discrete mathematics and program correctness at the same time! I've been looking for an excuse to (re)learn discrete math, and this looks like just the thing :-)

On a broader (slightly off-topic) note, I can't help but think that the usefulness of computer tools in teaching technical subjects in general (especially mathematics) has been largely unrealized. Most math students learn to use Mathematica and/or Maple to do symbolic manipulations, and maybe Matlab to do number crunching, but I'd like to see computer environments become an essential element in teaching mathematics at all levels. Many students conclude that they are "not good in math" because they aren't good at doing large amounts of error-free symbol manipulation on paper (exactly what computers are good at). The Beseme project is interesting precisely because it uses computer languages to facilitate learning in an area of mathematics where traditional computer algebra environments are less useful (proofs).

Noel Welsh - Re: Beseme Project Overview  blueArrow
11/23/2001; 8:04:12 AM (reads: 1594, responses: 0)
In response to Luke Gorrie's question, reasoning about programs is all about having a formal representation for the semantics of your program and then manipulating said representation to prove some desired result. FP is better because the formal semantics are simpler. I'm not aware of any formal semantics for C++ for example - it's just too darned complex.

I can think of a few examples where testing doesn't cut it, in addition to Ehud's example of security. A classic example is concurrency, where testing often doesn't show rare race conditions. With a formal calculus of concurrency (say, CSP, maybe the pi-calculus?) you could prove a program free of race conditions. Erlang (which I suspect Luke can tell us a bit about ;) is based on CSP. Another example that comes to mind is the data mining software I develop at work. This sort of program is designed to extract interesting features from data. It's very hard to test (except with very simple test data) because you never know if your implementation is buggy or your data simply has no interesting features. It would be nice to be able to prove that the program is correct (ie it is equivalent to the published algorithm). Existing FP hasn't tended to concentrate on numerics so this area is a bit weak.

And now for something completely different...

I see XP in part as a reaction to the onerous heavyweight processes of Rational UP and the ilk. However I think XP is more than a reaction to RUP; it is as much philosophy as methodology. To accept XP you have to take a very open and flexible approach to life, which naturally doesn't suit some people. No doubt all methodologies have their associated culture/philosophy but I don't see this as clearly as I do with XP. The XP maxim "do the simplest thing that could work" is _all_ about aesthetic decisions: beauty and craftmanship! When did you last see that mentioned in a Rational tome? This is interesting to me. I'm not sure why yet, but I think it ties in to ideas about creativity and skill mastery. People who have mastered a skill use that skill intuitively and are often unable to explain why they do things the way they do. XP seems to be pushing one to operate at this level, where decisions are intuitive. It's kinda a Zen philosophy to programming - don't think, just react to the code.

Does that make sense?! :)

Ehud Lamm - Re: Beseme Project Overview  blueArrow
11/24/2001; 8:47:21 AM (reads: 1585, responses: 0)
I like the general principles of XP (eXtreme Programming). That's why I don't like the fanatics: By saying XP is the answer to all the problems in the software world they make it sound like snake oil.

Of the XP principles I am esp. fond of refactoring and the emphsis on unit testing. I don't think that unit tests should replace typing, nor do I think refactoring should replace design. But I do think these are useful techniques that are well worth using.

To make this a liitle more on topic for LtU: The Refactoring Browser is an interesting programming tool.

Ehud Lamm - Re: Beseme Project Overview  blueArrow
11/24/2001; 8:52:32 AM (reads: 1648, responses: 0)
I like to think about it this way. Inforammly reasoning about programs is about understanding what a piece of code does. Formally it is about being able to prove program properties.

A simple example: Imperative languages that don't allow you to mess with the for loop counter variable are easier to reason about. When you come across a for loop you can tell how many iterations are going to occur etc. This is good for understanding; it also makes the proof rule easier to formulate and use.

C style for loops are thus in some sense harder to reason about.