From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,c406e0c4a6eb74ed
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!news.glorb.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!feed2.news.rcn.net!rcn!feed3.news.rcn.net!not-for-mail
Sender: jsa@rigel.goldenthreadtech.com
Newsgroups: comp.lang.ada
Subject: Re: ADA Popularity Discussion Request
References: <49dc98cf.0408110556.18ae7df@posting.google.com>
 <m3isb2ey3w.fsf@rigel.goldenthreadtech.com>
 <hMnYc.1759$w%6.1486@newsread1.news.pas.earthlink.net>
 <m3656vfgmf.fsf@rigel.goldenthreadtech.com>
 <vpblkhspuA9F@eisner.encompasserve.org>
 <e749549b.0409051449.574ec9ce@posting.google.com>
 <vS8%c.69$xA1.4@newsread3.news.pas.earthlink.net> <1094529422.982635@yasure>
 <_xl%c.431$xA1.301@newsread3.news.pas.earthlink.net>
 <m3d60xdcpu.fsf@rigel.goldenthreadtech.com>
 <chmmu8$cgv$2@a1-hrz.uni-duisburg.de>
From: jayessay <nospam@foo.com>
Organization: Tangible
Date: 08 Sep 2004 12:04:33 -0400
Message-ID: <m3r7pcbvce.fsf@rigel.goldenthreadtech.com>
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: 
 DXC=`[9WM9Fn??[DY84Z?F]<?]0R]m=BkYWIW:6bU3OT9S9ZhCF8eBK1g5S^aM2i8keRm]8eU9IHVPL>_
X-Complaints-To: abuse@rcn.com
Xref: g2news1.google.com comp.lang.ada:3489
Date: 2004-09-08T12:04:33-04:00
List-Id: <comp.lang.ada>

Georg Bauhaus <sb463ba@l1-hrz.uni-duisburg.de> writes:

> jayessay <nospam@foo.com> wrote:
>  
> : If you wanted you could implement the whole Eiffel Dbc thing (and then
> : some) as a set of macros using CLOS within Common Lisp.  As I recall
> : now, someone actually did this (I will try to find it).
> 
> Whether you can implement static DbC in CLOS is the more intereisting
> question. Compare to SPARK.

Yes, that is exactly the idea.  You would create a set of macros to
allow a natural expression for this.  Macros do all their work at
compile time.  Macros are "just" functions which are code transformers
- you have the entire power of Lisp available and can write complete
compilers (lex -> syntax -> ast -> semantic analysis -> optimization
-> code generation) and have the result integrated transparently with
the rest of the language.

ACL2 is another example of this sort thing.  It is an applicative
system with type inference and theorem proving used by Motorola, AMD,
Rockwell Collins, et.al. for modeling and proving properties of
commercial microprocessors.


/Jon

-- 
'j' - a n t h o n y at romeo/charley/november com