Obviously mainstream statically typed languages can't formally verify all complex app behaviour. My frustration is more aimed at having time and energy wasted from runtime and test suite errors that can be easily caught with a basic type system with minimal effort e.g. null checks, function parameters are correct type.

Formal proof languages are a long way from being practical for regular apps, and require massive effort for diminishing returns, so we have to be practical to plug some of this gap with test cases and good enough type systems.

Once you've tested the complex things that (almost) no language has a type system able to express, you also have tested null checks, function parameter types, etc. by virtue of you needing to visit those situations in order to test the complex logic. This isn't a real problem.

What you might be trying to suggest, though, is that half-assed type systems are easier to understand for average developers, so they are more likely to use them correctly and thus feel the benefit from that? It is true that in order to write good tests you need to share a formal proof-esq mindset, and thus they are nearly as burdensome to write as using a formal proof language. In practice, a lot of developers don't grasp that and end up writing tests that serve no purpose. That is a good point.

I just don't find this in practice. For example, I've worked in multiple large Python projects with lots of test cases, and nobody is making the effort to check what happens when you pass incorrect types, badly formed input, and null values in different permutations to each function because it's too much effort and tedious. Most tests are happy path tests, a few error handling tests if you're lucky, for a few example values that are going to miss a lot of edges.

And let's be honest, it's common for parts of the code to have no tests at all because the deadline was too tight or it's deemed not important.

If you have a type system that lets you capture properties like "this parameter should not be null", why would you not leverage this? It's so easily in the sweet spot for me of minimal effort, high reward e.g. eliminates null errors, makes refactoring easier later, that I don't want to use languages that expect me to write test cases for this.

> half-assed type systems are easier to understand for average developers

Not sure why you call them that. Language designers are always trying find a sweet spot with their type systems, in terms of how hard it is to use and what payback you get. For example, once you try to capture even basic properties about e.g. the size/length of collections in the types, the burden on the dev gets unreasonable high very quickly (like requiring devs to write proofs). It's a choice to make them less powerful.

This seems like a roundabout way of confirming that what you are actually saying is that half-assed type systems are much easier to grasp for average developers, and thus they find them to be beneficial because being able to grasp it means they are able to use it correctly. You are absolutely right that most tests that get written (if they get written!) in the real world are essentially useless. Good tests require a mindset much like formal proofs, which, like writing true formal proofs, is really hard. I did already agree that this was a good point.

> Not sure why you call them that.

Why not? It gets the idea across enough, while being sufficiently off brand that it gets those who aren't here for the right reasons panties in a knot. Look, you don't have to sell me on static typing, even where not complete. I understand the benefits and bask in those benefits in my own code. But they are also completely oversold by hyper-emotional people who can't discern between true technical merit and their arbitrary feelings. Using such a term reveals where one is coming from. Those interested in the technical merit couldn't care less about what you call it. If someone reacts to the term, you know they aren't here in good faith and everything they say can be ignored.

Dynamic typing is on the other end of the spectrum. That is a huge pain precisely because there are no automated checks.

In between those two extremes there is an (subjective)sweet spot. Where you don't pay much at all in terms of overhead, but you get back a ton from the checks it provides.

To clarify, I think formal verification languages are too advanced for almost everyone and overkill for almost every mainstream app. And type systems like we have in Rust, TypeScript and OCaml seem a reasonable effort/reward sweet spot for all levels of developer and most projects.

What's your ideal set up then? What type system complexity (or maybe language)? How extensive should the test suite be? What categories of errors should be left to the type system and which ones for the test suite?

That's not true. At no point in testing `fn add(a: i32, b: i32) -> i32` am I going to call `add("a", "b")` or `add(2, None)`. Rust even won't permit me to try. In a language with a more permissive type system, I would have to add additional tests to check cases where parameters are null or of the wrong type.

It seems you either don't understand the topic of discussion or don't understand testing (see previous comment). If the user of your function calls it in undocumented ways, that's their problem, not yours. That is for their tests to reason with.

Passing the wrong types is only your problem for the functions you call. Continuing with your example, consider that you accidentally wrote (where the compiler doesn't apply type checking):

    fn double(a: i32) -> i32 {
        add(a, None) // Should have been add(a, a)
    }

    // apply special discount
    newPaymentInfo = {value: oldPaymentInfo.value / 2}
    newPaymentInfo[tax] = applyRegionalTax(newPaymentInfo.value)
    return newPaymentInfo

    // apply tax to tips only in some regions
    if (taxableTips) {
        paymentInfo.tip += applyRegionalTax(paymentInfo.value)
        // ERROR: tip is undefined (instead of zero)
    }

If it's practical to get a static type system to exhaustively check a property for you (like null checks), it's reckless in my opinion to rely on a test suite for that.

> If the user of your function calls it in undocumented ways, that's their problem, not yours.

Sounds reckless to me as well because you should assume functions have bugs and will also be passed bad inputs. If a bug makes a function return a bad output, and that gets passed to another function in a way that gives "undocumented" behaviour, I'd much prefer to code to fail or not compile at all, because when this gets missed in tests it'll eventually trigger on production.

I view it like the Swiss cheese model (mentioned elsewhere), where you try to catch bugs at a type checking layer, a test suite layer, code review, manual QA, runtime monitoring etc. and you should assume flaws at all layers. I see no good reason to skip the type checking layer.

[1] https://jspecify.dev/about/

Lots of languages other than Rust have static types, some more complete than others.

Hardly. Suppose all caught errors in a particular module of code bubble up to a call site which (say) retries with exponential back-off. If the compiler can guarantee that I handle every error, I only need one test that checks whether the exponential back-off logic works. With no error handling guarantee, I'd need to test that every error case is correctly caught—otherwise my output might be corrupted.

No matter how you slice it you have to figure out what the software you are calling upon does and how it is intended to function. Which is, too, why you are writing tests: So that your users have documentation to learn that information from. That is what tests are for. That is what testing is all about! That it is also executable is merely to prove that what is documented is true.

All languages with exceptions enter the chat

Let us introduce you to the concept of checked exceptions. That is one of the few paradigms we've seen in actually-used languages (namely Java) where communicating which specific errors will occur has been tried.

Why is it that developer brains shut off as soon as they see the word "error"? It happens every time without fail.

Snubbing type systems because they aren't 100% failproof misses that point.

[0] https://en.m.wikipedia.org/wiki/Swiss_cheese_model