From: gabriele renzi <surrender_itRemove@...>
Date: 2006-08-09T03:50:10+09:00
Subject: Re: Language chatter

Francis Cianfrocca ha scritto:
> On 8/8/06, M. Edward (Ed) Borasky <znmeb@cesmail.net> wrote:
>  >
> 
>> I learned Lisp (1.5) in the early 1970s, and this style of programming
>> seemed to be tied to Lisp at the time, but I actually had used it
>> earlier. For some reason FORTRAN programmers, including myself when I
>> was one, don't usually use this style, perhaps because the original
>> FORTRAN didn't have structured concepts and forced the use of GO TO
>> statements.
> 
> 
> 
> I've always been fascinated by one specific aspect of functional
> languages: in theory, it's possible to use tools to prove programs
> correct. What a productivity win that would be. 

notice that to proof some properties of a program you don't necessarily 
need a functional language.
For example, you may love to take a look at Spark[1], a statically 
verifiable subset of Ada, or at Vault[2].

Other languages can proof correctness for "some"functionalities.
I had the chance to work with NesC[3] wich is a nifty language for 
embbeded systems, basically C+concurrency+components, where the compiler 
checks that there are no race conditions in concurrent code (it gets 
some false positives, but no wrong code passes).

[1] http://www.praxis-his.com/sparkada/intro.asp
[2] http://research.microsoft.com/vault/intro_page.htm
[2] http://nescc.sourceforge.net/