On Fri, Oct 3, 2008 at 6:39 PM, <ajb@spamcop.net> wrote:
G'day all.

Quoting Don Stewart <dons@galois.com>:

How about EDSLs for producing high assurance controllers, and other
robust devices they might need. I imagine the LHC has a good need for
verified software components...

On a related topic, I'm curious if anyone apart from me has been secretly
using Haskell for model-driven-development-lite.

My current boss, not being a programmer, doesn't care where the code
comes from, so the following conversation is unlikely to happen.  Still.
other people must also have thought of doing this:

"Well, the reason why I've produced so much C++ lately is because I've
been generating all the boilerplate automatically.  What with?  Glad
you asked..."

Replace C++ with python and you have what I've been thinking about.  I've been of several minds:
1) Write a type checker for python in Haskell
2) Write a Haskell program that reads special "type" comments from python programs and type checks the python
3) Write a python generating EDSL in Haskell
4) Translate Haskell to python

Python is what we typically use for various technical reasons, but I'm quite unsatisfied with it.  Every time I turn around I'm faced with learning a new facet of the language (or less politely, a limitation it has that I wasn't expecting).  I also find that I spend a lot of time trying to figure out ways to hit the various control paths, otherwise I rely on tools like pylint, which don't work so well.  When, I'm often just looking for type incorrect statements and misspelled variable names.  Really, if I had more static analysis, I'd have to do less of what the compiler could be doing.  I think testing is often easier in Haskell too, but maybe that's just my opinion.

The problem with #1 is that others have tried it, python just doesn't lend itself to type checking.  The problem with #2 is that I'm no longer writing python, I'm writing my version of python and other devs on our team could object, and some of the problems with #1 may apply.  None of those are strong arguements against it.  The main problem with #3, is that if I share code with other devs they have to learn Haskell and my EDSL since they won't be able to just hack the generated python, similar problem with #4.  Also, problem with #4 is that it may be difficult to generate efficient idomatic python code.

At my company, the source code is often a deliverable it seems that I can really only do #1 and #2 and I'm not convinced it's worth the effort.  I'd probably better off making a tool that can read in a python program and generate test cases to correspond to the work that static analysis would be doing.  This is the first time this idea has occured to me, but I like it and I should spend some more time thinking about it.  Is it possible to make a test case generator that can generate test cases to hit each execution branch in a program?  Oh, but maybe I could use such a program to solve the halting problem?  If so, that would be a useful application as well :)

Fundamentally, I think I agree with your approach assuming the political and team aspects work out.  If you're the only one that is willing to use language X on the team then it seems like bad form to use language X when you know you have a team to work with.  Sometimes being a team player is way more important than the technical details, or so I've found.

Jason