5 ms·
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.
by linuxlizard 6y ago
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.
- Jtsummers 6y agoIf 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.
- cb321 6y agoNim 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 https://nim-lang.github.io/Nim/drnim.html [2] https://blag.cedeela.fr/curry-howard-scam https://blag.cedeela.fr/curry-howard-scam
- Jtsummers 6y agoInteresting, 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.
- cb321 6y agoMany Nim things are works in progress. If passionate & capable people like yourself contribute, the finish line will seem that much closer. :-)