From: Stephen Leake <stephen_leake@stephe-leake.org>
Subject: Re: SPARK and unbounded tree structures
Date: Thu, 11 Jun 2009 06:31:53 -0400
Date: 2009-06-11T06:31:53-04:00 [thread overview]
Message-ID: <uzlcfrrhi.fsf@stephe-leake.org> (raw)
In-Reply-To: 06f0b9ca-3c00-44e8-9a52-63c840ed0abe@21g2000vbk.googlegroups.com
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
prev parent reply other threads:[~2009-06-11 10:31 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-10 16:52 SPARK and unbounded tree structures xorquewasp
2009-06-11 7:35 ` Rod Chapman
2009-06-11 8:28 ` Phil Thornley
2009-06-11 8:43 ` xorque
2009-06-11 10:31 ` Stephen Leake [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox