On: Formal methods only solve half my problems

[csours]

The longer I spend in IT/Software Dev, the more I see a dichotomy between Correctness and Usefulness. You can certainly have both, but different people concentrate on either correctness or usefulness. I think the future of software dev is people who understand both.

[justahuman74 → csours]

The tools make it very hard to do both at the same time. To pick a topic, is there something I could write shell-style scripts in that leans towards correctness?

[pharmakom → justahuman74]

Yes! F# scripts

Some features:

- open-source

- cross-platform

- quick editing with syntax highlighting, type annotations etc. in VS Code

- run in a single command (‘dotnet fsi script.fsx’)

- type-safe but with global type inference

- grab dependencies using directives in the script (no project manifests or global dependencies)

The added safety of a typed language is fantastic for scripting because it’s not worth writing tests for most scripts.

[simonmic → justahuman74]

Haskell (using https://docs.haskellstack.org/en/stable/GUIDE/#script-interp...).

The downside: requires 1. installing stack and 2. waiting for it to install ghc and libs on first run of the script.

[csours → justahuman74]

Correctness needs a specification. Correctness hates side effects. Shell type scripts are all about side effects.