Comment by elcritch | Hacker News Reader

Comment by elcritch | Hacker News Reader

Nim despite having Python like syntax inherits much from Pascal. It was even originally written in FreePascal [1]!

I've come to appreciate `var` and `let` blocks in Nim that I believe come from Pascal syntax:

    let
      mnist = load_mnist(cache = true)
      # Training data is 60k 28x28 greyscale images from 0-255 
      # Change shape from [N, H, W] to [N, C, H, W], with C = 1 (unsqueeze). Convolution expect 4d tensors
      X_train = ctx.variable x_train.unsqueeze(1)
      ...

However unlike Pascal syntaxes (and Ada), Nim remains less verbose and feels less "straight jacketed" for it. It's odd but while it encourages safer code than C its doesn't feel quite as stifling. You can do most any pointer manipulations you might need, but using builtin functions (i.e. `addr` or `unsafeAddr`) rather than symbol operators.

1: https://news.ycombinator.com/item?id=25242926 2: https://github.com/mratsim/Arraymancer/blob/master/examples/...

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);
      ...

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