On Wed, 17 Feb 1999, George Beshers wrote:
> 1. If the tool can resolve the types (and I would expect this
> to be true most of the time) it can display the types and (if
> the user or style guide dictates) add the types to the source.
>
> 2. If the tool can not resolve the type of a particular
> construct then the programmer can add the information and
> the tool can verify that the supplied type is correct.
>
> 3. As D. Tweed's short STL example points out, C++ can be all
> but unreadable without the support of static analysis tools
> today (oohhhhh... there was an implicit constructor call there!!!).
> I would argue that working with large software systems in any
> language requires support from software tools. So why not
> design Haskell-2 with tools in mind?
>
For anyone who would like to see what a tool like this *might* look like I
think you should look at Alfa. This tool is really a proof editor but
could as well be used as a programming tool for the functional language
cayenne since the proofs are formulated in cayenne and proof checking is
done by typechecking the program/proof. This can be be done because
cayenne is a language with dependent types which are powerful enough to
express just about anything about the program. The typechecking is done
incrementally which is really neat and prevents you from constructing
erronious proofs/programs. Alfa has a GUI which is really nice and allows
you to just use the mouse for programming/proof construction.
Alfa can be found on:
http://www.cs.chalmers.se/~hallgren/Alfa/
/Josef
----------------------------------------------------------
|Josef Svenningsson|http://www.dtek.chalmers.se/~d95josef|
|Rubingatan 39 | email: [EMAIL PROTECTED] |
|421 62 Göteborg | tel: 031-7090774 |
----------------------------------------------------------
What is a magician but a practising theorist?
-- Obi-Wan Kenobi
