Hacker News Reader

Was hoping someone would mention Ada. It's the most Pascal-y of all Pascal's children. I enjoyed my brief time doing Ada. I should look at Nim.

View on HN

If it's been a while, SPARK/Ada has been interesting to play with. No real objective for me since work won't touch it, but it's been interesting playing with the prover and design-by-contract elements of it. It's more properly integrated (with Ada 2012) than the prior versions.

Nim is adding proof engine integration [1] { though it may not be for everyone/all circumstances [2] ;-) }.

[1] https://nim-lang.github.io/Nim/drnim.html

[2] https://blag.cedeela.fr/curry-howard-scam

Interesting, though that only seems to be a small subset of what SPARK does.

> DrNim currently only tries to prove array indexing or subrange checks, overflow errors are not prevented. Overflows will be checked for in the future.

Those are the very basics of what you might use SPARK for, but it can be used for deeper proofs of your program invariants as well.

Many Nim things are works in progress. If passionate & capable people like yourself contribute, the finish line will seem that much closer. :-)

Reply on news.ycombinator.com