Hacker News Reader

Comment by pdw | Hacker News Reader

That's more likely copied from the functional programming world (ML / Miranda / Haskell). And they got it from Lisp's "let" form.

Wirth's languages always had a very strict separation between variable declarations and code. Your example might look something like this in Pascal:

    PROCEDURE foo;
    VAR mnist: MNistRecord;
        x_train: XTrainRecord;
    BEGIN
      mnist := load_mnist(true);
      ...

View on HN

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.

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