Hacker News Reader

But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.

With SPARK mode you can check them at compile-time with provers and elide the runtime checks. You can do _very_ sophisticated type predicates this way.

Reply on news.ycombinator.com