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/5288 https://github.com/coq/coq/issues/6768 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 ;)
> 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".
Well I strongly agree with that if you meant strongly statically type programming languages. I think they're a good sweet spot and I'd pick them over dynamic languages even for small projects.
The reason I went down the route of software verification is you said "In fact, my experience with "advanced type systems" (e.g. Agda, Idris and Coq)". Wouldn't OCaml or Haskell have been better examples? Why use Agda, Idris and Coq at all if you're not going to prove advanced program properties?
I would say Coq is used solely for software verification with the help of dependent types, while Agda and Idris are an attempt to make software verification with dependent types more palatable. I'm not sure why you'd use them over OCaml or Haskell if you weren't going to use types that were more advanced.
> 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:
How often are you really doing non-structural recursion though? It's exceptionally rare to write complex loops like a GCD algorithm was my point. Either way, I agree an escape hatch for proving properties can be a practical solution.
> Wouldn't OCaml or Haskell have been better examples? Why use Agda, Idris and Coq at all if you're not going to prove advanced program properties?
Why not? Just because they have advanced type systems doesn't mean that we need to make use of those features; the same way writing a Haskell program doesn't require us to use closed type families, multi-parameter type classes with functional dependencies, etc. or OCaml doesn't require everything to be an applicative functor over a row-polymorphic existential, etc.
As an aside, when I am doing fancy things with types, I personally find dependent types much simpler to think about and work with than the tower of cards that Haskell and GHC have been building via language extensions. The downside is limited type inference :(
In any case I was trying to highlight the common implicit assumption that programs written in languages with feature X (like powerful types) must therefore use feature X. There's no reason for that to be the case: programs in Haskell and OCaml can be stringly typed, so can those in Coq and Idris. Yet this clouds comparisons, where on one side we might have a formally verified microkernel, and on the other we might have a pile of bash string interpolations.
I will readily admit that Coq would be a pretty horrible choice for writing regular software, but mostly due to ergonomics like having multiple nested languages (vernacular, gallina and ltac) and having to "extract" programs to run them. On the other hand I think Idris is really nice, and would enjoy using it for projects which don't rely on some exising library infrastructure.
> How often are you really doing non-structural recursion though? It's exceptionally rare to write complex loops like a GCD algorithm was my point.
It's definitely a small fraction of the number of `map` or `fold` calls I write, but it's not insignificant. I worked on a project recently that made heavy use of sets, so there was a lot of sorting going on which IIRC wasn't structurally recursive; it also calculated least common multiples (similar to greatest common divisor) as part of a random sampling function. That project was in Racket though :P
> Either way, I agree an escape hatch for proving properties can be a practical solution.
In Coq I often just stick on a decreasing "fuel" parameter, turn the result into an `option` and bail out with `none` if the fuel runs out :P