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