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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: example of machine generated Ada ?
Date: Fri, 09 Jan 2015 13:33:32 -0800
Organization: A noiseless patient Spider
Message-ID: <87ppanr64z.fsf@jester.gateway.sonic.net>
References: <87fee75d-04d9-49bb-8cb2-4c5ea7f98cdf@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="9be1734e45595b2e29ecbdd3ce926380";
	logging-data="21791"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+ZLhO4HFBkH5LeLRMVAyMY"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:b/3JoqgETkuhYgFmDaxarmUfpvc=
	sha1:RtHKe39fuJDrIC16gIkfV0scjm0=
Xref: news.eternal-september.org comp.lang.ada:24508
Date: 2015-01-09T13:33:32-08:00
List-Id: <comp.lang.ada>

Patrick <patrick@spellingbeewinnars.org> writes:
> Several languages use C as an intermediate language but hand written C
> is hard to read and machine generated is even more painful. Ada might
> make for reliable, readable machine generated code.

Pardon the response to a >1 year old post but ImProve can do this:

    https://github.com/tomahawkins/improve

Blurb from page:

    ImProve is an imperative programming language embedded in Haskell
    for high assurance applications. ImProve uses infinite state,
    unbounded model checking to verify programs adhere to
    specifications. Yices (required) is the backend SMT solver.

    ImProve compiles to C, Ada, Simulink, and Modelica for
    implementation and system simulation.

I've played with it a little bit and also with the author's other
language, Atom.