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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.99.116.7 with SMTP id p7mr27034643pgc.109.1481675933832; Tue, 13 Dec 2016 16:38:53 -0800 (PST) X-Received: by 10.157.18.211 with SMTP id g77mr6549061otg.14.1481675933726; Tue, 13 Dec 2016 16:38:53 -0800 (PST) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!border1.nntp.ams1.giganews.com!border2.nntp.ams1.giganews.com!nntp.giganews.com!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.am4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!p16no78524qta.1!news-out.google.com!m27ni1065qtf.1!nntp.google.com!n6no79548qtd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 13 Dec 2016 16:38:53 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=67.0.242.189; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 67.0.242.189 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <3f93063b-d287-4e48-966f-555189bfe185@googlegroups.com> Subject: Re: Ada 2012 Constraints (WRT an Ada IR) From: Shark8 Injection-Date: Wed, 14 Dec 2016 00:38:53 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 2965 X-Received-Body-CRC: 142496358 Xref: news.eternal-september.org comp.lang.ada:32803 Date: 2016-12-13T16:38:53-08:00 List-Id: On Tuesday, December 13, 2016 at 3:35:27 PM UTC-7, Randy Brukardt wrote: >=20 > Surely not a bad idea, but I think it's likely to be impractical. Certainly where the thrust for my original posting here was going: a unifie= d yet general IR with respect to constraints would make things much nicer f= or a SPARK-like tool... and it's not unreasonable that you could get some o= f SPARK's advantages w/o some of its restrictions. (Just like you point out below for optimizations.) > I suppose if someone started from scratch with proof in mind, they could > replace a lot of optimization code with proof -- but is anyone really > going to start a project like that from scratch these days? (Having a > proof engine is not going to make Ada visibility and resolution any > easier to implement.) Well, I've already started on Byron[1], a compiler for Ada 2012 in Ada 2012= , which does aim for being provable where possible. -- And I'd always had a= n IR like this in mind before even starting. -- It would be nice to integra= te an SMT into it, but I think implementing an SMT is beyond my current abi= lities. (And the reason I'm assuming that I'd have to be the one to do it i= s because, so far, I'm the only contributor to the project.) I do 'cheat' a little bit with the lexer, the only phase that's complete ri= ght now... actually, I think you'd find it humorous to see how I did it. (A= nd yes, there's some ugly code and ordering dependencies in it... the good = news is that it can easily be replaced so long as the replacement emits tok= ens properly/consistently w/ the token packages.) [1] -- https://github.com/OneWingedShark/Byron