Re: How to get Ada to “cross the chasm”?

[Paul Rubin <no.email@nospam.invalid>]

Shark8 <onewingedshark@gmail.com> writes:
> for an Ada+VHDL IDE

Dan'l Miller also mentioned Ada+VHDL.  What is it?  I don't see many
search results.  Of course there is a well-known general resemblance
between Ada and VHDL, but I don't know of any meaningful composition of
them.

> - Written in 100% Ada; SPARK proving for the compiler-proper.

Why would you want to do that, when a ton of SPARK verification
conditions are about proving integer overflow safety, memory
boundedness, and other freedom from exceptions?  E.g. I think it stops
you from using natural programming techniques like recursion (at least,
MISRA C does not allow recursion).  That is all crucial for realtime
systems, but a compiler is not a realtime system.

If you use CompCert's approach (use recursion and unbounded arithmetic
and automatic memory management in the compiler as much as you want,
prove that the compiler won't generate bad code, use ordinary software
testing to give reasonable assurance that the compiler doesn't crash,
and call it a day) you can probably save a heck of a lot of work.

Is it even possible to guarantee that a compiler can accept every valid
program and also never crash?  If Ada programs can have nested
parenthesized expressions or begin/end blocks of arbitrary depth, then
any sane approach to parsing will eventually run out of memory if the
nesting is deep enough.

CompCert itself is already a magnificant feat.  I have no idea whether a
fully proven compiler in SPARK is feasible at all.  Has anyone ever done
anything like that?

> - Application of SPARK provers to VHDL.

Does anyone do that?  There's some work on HDL verification but it uses
completely different approaches.