Functional programming languages & formal verification 
Author Message
 Functional programming languages & formal verification

Has anyone used FORTH as a functional language?  Regarding F-PC 3.55,  
someone had described FORTH as a highly structured languages with no  
gotos, and only one entry and exit point... which made me think that  
perhaps FORTH could be used as a functional language.  Of course, 1 2 + is  
equivelant to +(1 2) and so on.  Perhaps this would make FORTH programs  
easier to verify.  Formal verifcation is especially needed in the  
application domains FORTH is used in (i.e. real-time, embedded stuff that  
could really hurt someone!)  Furthermore, FORTH (I would imagine) would be  
much more efficient than some versions of some functional languages seem  
to be.


Wed, 18 Sep 1996 05:27:57 GMT  
 Functional programming languages & formal verification

Quote:

>Has anyone used FORTH as a functional language?  Regarding F-PC 3.55,  
>someone had described FORTH as a highly structured languages with no  
>gotos, and only one entry and exit point... which made me think that  
>perhaps FORTH could be used as a functional language.  Of course, 1 2 + is  
>equivelant to +(1 2) and so on.  Perhaps this would make FORTH programs  
>easier to verify.  Formal verifcation is especially needed in the  
>application domains FORTH is used in (i.e. real-time, embedded stuff that  
>could really hurt someone!)  Furthermore, FORTH (I would imagine) would be  
>much more efficient than some versions of some functional languages seem  
>to be.

Look up:

Baker, H.G.  Linear Logic and Permutation Stacks -- The Forth Shall Be
First.  Computer Architecture News 22,1 (March 1994), 34-43.

It gives examples in postscript, since it is the only Forth-like
language I have access to.  It has a very long set of references,
including those to functional Forths -- e.g., Koopman's 1989 book
"Stack Computers, The New Wave" and his PhD thesis at CMU on
functional languages using Forth-like architectures.

I believe that I have recently seen postings by Koopman, so he'll
probably see this.



Thu, 19 Sep 1996 03:28:16 GMT  
 Functional programming languages & formal verification

Quote:
> Has anyone used FORTH as a functional language?  Regarding F-PC 3.55,  
> someone had described FORTH as a highly structured languages with no  
> gotos, and only one entry and exit point... which made me think that  
> perhaps FORTH could be used as a functional language.

I wonder why people keep considering FORTH a highly structured
language...  You can have multiple exit points trivially, and can even
muck with the return stack.  Some have even claimed that because FORTH
doesn't have a GOTO, and there are versions of Pascal that have GOTOs,
that therefore FORTH is more structured than Pascal.  I would doubt
that FORTH programmers are more disciplined than others to not use a
questionable features.  Sorry, but the Emperor is shivering.
--
Darin Johnson

  - I'm not a well adjusted person, but I play one on the net.


Thu, 19 Sep 1996 10:03:23 GMT  
 Functional programming languages & formal verification

Quote:

> >Has anyone used FORTH as a functional language?  Regarding F-PC 3.55,  
> >someone had described FORTH as a highly structured languages with no  
> >gotos, and only one entry and exit point... which made me think that  
> >perhaps FORTH could be used as a functional language.  Of course, 1 2 +  
is  
> >equivelant to +(1 2) and so on.  Perhaps this would make FORTH programs  
> >easier to verify.  Formal verifcation is especially needed in the  
> >application domains FORTH is used in (i.e. real-time, embedded stuff  
that  
> >could really hurt someone!)  Furthermore, FORTH (I would imagine) would  
be  
> >much more efficient than some versions of some functional languages  
seem  
> >to be.

I used Forth as a target language for translation from a functional  
language. The functional language was D/M, of my own design. This  
translation is straightforward. Of course, verification of programs in  
functional languages is at least a more understandable task. (I am not  
saying simpler.) This is also true to Forth when it is used as a  
functional language. Although, Forth is richer than its functional  
constituent - i am recalling pictures from Thinking Forth.

Usually inefficiency of functional languages comes from a heavy use of  
complex data structures for all purposes. If a functional language takes  
advantage of simpler aggregate data, it can be as efficient as Forth.

Alex Sakharov

Motorola, Inc.                          Voice: (708)576-4465
3701 Algonquin Rd., Suite 600           Fax: (708)576-2025



Fri, 20 Sep 1996 23:58:30 GMT  
 
 [ 4 post ] 

 Relevant Pages 

1. IBM/Israel: Open Positions in Functional Formal Verification

2. BACUP meeting: Formal Verification, Physical Verification; SourceLink

3. BACUP meeting: Formal Verification, Physical Verification; SourceLink

4. Animation of formal specifications in a functional language

5. numerical & statistical programming in functional languages

6. Verification of functional programs

7. Formal verification methods for OOPS

8. Formal methods for verification of OOPS

9. Scientific puzzle of formal circuit verification at next week's DAC

10. Formal verification of one-hot state machine.

11. Formal Verification

12. Formal verification

 

 
Powered by phpBB® Forum Software