Thanks for the info about seL4, I hadn't seen those effort estimates before.

However, I don't think it's relevant to the point I was making. You seem to be talking about formally proving things. If you look through my comment that you're replying to, you'll see that I don't talk about proving anything, let alone "complicated software properties".

I was talking about writing programs in languages with 'advanced type systems', as opposed to dynamically typed languages; and that I've not seen compelling evidence to back up common claims like "dynamic languages are faster to program in".

You've given compelling evidence that "formally verifying complex properties of large systems is slow and hard", which I think many would already agree with. That doesn't seem relevant to the typed/untyped programming comparison, since formal verification is still a very uncommon thing to do (ignoring language-provided guarantees like memory safety or type safety).

> proofs are done with Isabelle so it's not using types for proofs like e.g. Coq does but you can't escape a similar verification effort

I don't understand what you mean by "you can't escape a similar verification effort". Not only was I not talking about proving anything, I even stated that the type system can often be ignored and gave "stringly typed programming" as an example (where a program is strongly typed, but almost everything has type `String`, which gives us something quite close to a dynamically typed language; including no guarantees that our variables even have meaningful contents, let alone for any "complicated program properties"!).

> Why do you think function termination checking is a big factor? I find the majority of loops in apps are of the form "for everything in this collection" or a similar restriction that is simple to check.

I tend to write in a functional programming style, which makes heavy use of recursion.

Termination checking (AFAIK) doesn't have the same sort of powerful, composable nature that type checking has, so languages like Coq and Agda (which require termination checking) are very conservative in whether to allow certain forms of recursion or not. It's easy to do "structural recursion", where recursive calls are run on a sub-expression of the argument, e.g.

odd Zero = False
odd (Succ n) = not (odd n)

It's harder to do non-structural recursion, where the recursive call isn't acting directly on part of the argument, e.g. the greatest common divisor algorithm:

gcd a 0 = a
gcd a b = gcd b (mod a b)

This requires ad-hoc proofs to convince the system that the arguments are getting "smaller" by some measure (in this case the sum `a + b` always gets smaller). These can get very hairy, and don't really compose. In this case, for the system to accept the above definition of `gcd` we need to go off and prove theorems about `mod` (i.e. that `b > 0 -> mod a b < b`).

The hardest cases I tend to run into are co-termination, which Coq is especially bad at, both in practice (co-recursive calls must be manually unwrapped, and there doesn't seem to be any way to abstract over the raw `cofix` form) and in theory ( https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/6768 ). Agda's co-patterns are nicer to work with, but still require weird type-level hacks (like the "sharp" and "flat" operators, "sized types", etc.)

When languages require termination, these sorts of overly-conservative restrictions are inevitable, and we have to deal with them regardless of whether we actually care about termination (or type soundness). That's why I like programming in languages like Idris, where we can selectively ignore termination, and hence the restrictions on what forms we're allowed to write.

> What properties were you proving with types where you say they weren't getting in the way?

I wasn't talking about proving anything, using types or otherwise. I was specifically talking about not proving things, despite the type system allowing us to do so if we want to (which, if we're happy to consider dynamic types, we probably don't want to).

However, when I do happen to be using types to prove things (which, again, is absolutely not required at all, whether or not we're using an 'advanced type system') I find it hard to say that types are "getting in the way", since they're the system of logic for the proofs. We could get such types 'out of the way', but that would also throw away the point of the endeavour. After all, we can 'prove' all sorts of things if we don't allow logic to get in the way ;)