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-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news2.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail Newsgroups: comp.lang.ada Subject: Re: SPARK and unbounded tree structures References: <06f0b9ca-3c00-44e8-9a52-63c840ed0abe@21g2000vbk.googlegroups.com> From: Stephen Leake Date: Thu, 11 Jun 2009 06:31:53 -0400 Message-ID: User-Agent: Gnus/5.11 (Gnus v5.11) Emacs/22.2 (windows-nt) Cancel-Lock: sha1:P0+cnUKl5sZwr1c2lmictwYVwQc= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Complaints-To: abuse@flashnewsgroups.com Organization: FlashNewsgroups.com X-Trace: 188414a30dd03e9cadf9d32731 Xref: g2news2.google.com comp.lang.ada:6433 Date: 2009-06-11T06:31:53-04:00 List-Id: xorquewasp@googlemail.com writes: > I'm going to be working on a compiler for a domain-specific functional > language soon. For obvious reasons, I'd like to use SPARK, if > possible. Ada is an obvious choice for this project, but SPARK is not. SPARK is a good fit for _high integrity_ software, where you _must_ be able to prove precise statements about the program's behavior. Compilers are not that. They are far too complex for tools like SPARK to handle (given the current state of the art), only in part because of the problem you cite here. All compilers have bugs. That's the state of the art. That's why users must test their code, and assume the compiler has bugs. -- -- Stephe