Why I still Lisp

> And such errors happen all the time, the same way without syntax checks typos happen all the time.

No they don't, because syntax is richly varied and nested, even in programs whose "type story" is bland.

For instance, in some numerical program, there are lots of opportunities to make typos in the syntax, but the type of just about everything may be either float or else array of float (possiby string, if it has any error-handling code with messages, and bool if there are some logical operations).

If you pass an array of float where a scalar float is expected, such that an error occurs, and if you don't catch this in your testing, it means you're not testing the code.

Untested code is of a dubious status, even if it compiles with a static type system; testing is not negotiable.

Note that functions like sin and cos have exactly the same type signature, yet it is disastrous if you mix them up. Static type checking doesn't help. Static type checking also doesn't help with mixed up variables: calling f(x, y) which should have been f(y, x) or something else, where x and y have the same type.

In programs, chunks of code that are put together into the same module or function often work with multiple instances of the same type. It's more important not to mix up those instances, than to worry about type errors. The code could be wrong in all sorts of ways, yet statically check.

That's where you need to step up the the argument into "True Scotsman's type systems territory": a sufficiently advanced type system can encode all those properties that prevent the mixups that the everyday type system doesn't. Yeah, well, nobody uses that; nobody understands it outside of a narrow slice of academia. Examples of the technique are such that encoding even a trivial property like "list is in sorted order" results in an a considerable increase of program complexity all concentrated in one place, and less easy to understand than a set of test cases against the obvious program. Yet, it doesn't eliminate the need for testing; nothing does. There can now be a bug in the way the desired property was encoded into the program. Perhaps the sorted property was correctly encoded, but it should have been descending order. The test case will catch it.

When you have a language that is available at compile time, you can execute test cases as part of compilation. Test cases are therefore static checks. Anything happening at build time is a static check. Heck, how a git commit message is formatted is a static check, if a repository commit hook validates it.

Personally, I consider teaching the lambda calculus to be a real-life situation. Teaching the lambda calculus is no less real to me than any other part of my life. But OK, self-apply is not something you're likely to see in production code, and neither are Church numerals, which is where this problem shows up for real. But MAP, REDUCE, and APPLY are, and they all have the same problem as self-apply: their static types are infinite.

This is a general problem with all static type systems. There are only two possibilities: either your type system is Turing complete or it is not. If it is not, then there are things that one might reasonably want to express that cannot be expressed, and if it is, then it is undecidable. Static typing is either constraining, or it is a Turing Tarpit (https://en.wikipedia.org/wiki/Turing_tarpit).

Yes, frameworks are kind of like a smarter programmer starting you off with a code base already, so if you don't really know what you're doing you can't mess it up as much. I've still seen people mess it up, and generally it's when the developers begin to "play" with things they don't understand, like bringing in Aspect J, writing custom annotations, slowly moving logic to configuration files, starting to dynamically load modules in/out.

It's a bit of a struggle because an experienced dev will hate the framework, as they know better, but then as less experienced dev work on the code base it'll degenerate in a way the framework would have survived longer due to availability of documentation and Stackoverflow Q/A.

> I started serious programming in my teens in BASIC on a ZX Spectrum+, although I had previously dabbled in (hand-) writing Fortran programs

> I ended up studying Programming Languages at Indiana University with Dan Friedman (of The Little Lisper / The Little Schemer fame). It was my introduction to Scheme (and the world of Lisp.) I finally knew that I had found the perfect medium to express my programs in. And it has not changed in those last 25 years

Author seems to have over 25 years of experience.

The auto-completion is purely Python's dynamic-dispatch problem though. Lisp has symbol-based auto-completion which doesn't suffer from the same issue (search is a different story!).

This sounds terribly controversial, but I would love to know /when/ the static-typing pays off compared to a looser approach like sound-gradual typing (where you basically export types at a boundary and make sure that you don't violate those).

I do wonder whether a better approach is to prove your code in some other language (say Z3, Agda, Coq) - then implement it in something else, making sure you can prove isomorphism. This has quite a few benefits; you're not tied to a constructive proof on the type-level ala Haskell, Rust, Go etc... and you can automate a large part of trivial proofs.