News for hackers. Stuff that matters.
Re:Types as Interfaces by kqr on Tuesday July 23, 2024 @09:04AM (#41045554)
But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.
Re:Types as Interfaces by docandrew on Tuesday July 23, 2024 @09:13AM (#41045646)
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.