I thought Ada did only runtime checks? I am asking for (and my template hackery implements) compile-time checks. Runtime checks are slow and don't fully mitigate security bugs, though they probably downgrade the bugs to DoS attacks. But if these are actually checked by the compiler, that's pretty cool and I might actually have to play with Ada at some point!

First, generalized static invariants that are either correct all the time or computable all the time are, impossible, of course. Even of the simple form you are trying. Second, Ada 2012 has static type invariants (enforced at compile time) and dynamic type invariants (enforced at runtime)

You should be able to do, at the very least, what you are doing, in a much simpler way.

Plus, it has procedure level pre and post conditions that are checked

In any case, the tools ADA has allows it to go further than what you want, actually. https://en.wikipedia.org/wiki/SPARK_(programming_language)

There is a formally verifiable language that is just a subset of ada (IE compilable as normal ada) but can formally verify what you want here even if static predicates can't.

(Now all of the above said, i'm not sure i'd go this route, but yeah)

Ada does a mix of both compile-time and run-time checks. It was systematically designed to eliminate errors in most parts of the development process as the book below shows. SPARK, an Ada variant, can prove absence of all kinds of errors in code with automated provers. Since Ada supports cross-language programming, the typical route is to do most of the key logic in Ada, anything static/simple in SPARK, and anything platform-related in native language if too hard to do in Ada. They periodically update them with recent versions at 2012 for Ada and 2014 for SPARK.

http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book...

Note: See table of contents especially.

http://cowlark.com/2014-04-27-ada/index.html

Note: This "random walk through Ada" has a nice summary of all kinds of features it has from perspective of an outsider instead of an Ada developer.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

http://www.adacore.com/uploads/technical-papers/SPARKSkein_S...

Note: Link to SPARK and an example by Rod Chapman on doing Skein in it. Just converting it from C to SPARK found an error in original code. Because of course it did haha...

Idris or F*? I think they are not practical because compile times end up extremely slow. I think want you want will necessarily have this effect of very slow compile times.

Came here to suggest Idris, as it compiles to C. F* is still experimental and Idris is just coming up on a RC. They could also drop down into C and manually verify it.

What's the story for interop between Ada and C on modern systems? That is, if I want to write a library that C programmers on Ubuntu or something can use in a straightforward manner, can I write it in Ada without too much difficulty?

Ada was designed for cross-language development. It was ahead of the curve on that. I'd be surprised if it was hard to integrate C today. The others I recall off top of head that went big in industry were OpenVMS (standard calling conventions, etc) and .NET CLR. I can't find my original article on "mixed, language development" in Ada but the marketing piece below gives you an idea of what developers were doing in 2005. Mixed language development, debugging, and traces. It's probably better now.

https://www.rti.com/hubfs/docs/2005Q1_2.pdf

Ada95 added the Interfaces.C package for interop with C. http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-B-3.htm... shows the interface for Ada 2012. If you want your library to run anywhere then you probably still need to use C.

Does Ada check these type of invariants at compile-time or run-time?

It can do both.

Ada is not the right solution.

So what is the right solution? Don't leave us hanging like that, so unpolite.