[hope-striker]

1. Bidirectional typing can be easily generalized to dependent types. You can't always infer the type, but an 80% solution is definitely good enough for inference.

2. Your types don't have to be full specifications, and you can refine them later, no?

3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default.

4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like.

5. What are the competing approaches and how are they better at dealing with, for example, distributed computing?

I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.

[9q9]

1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature

   forall T.
       Array[T] -> 
       (T -> T -> Bool) -> 
       Array[T] 

Bidirectional will not infer what's missing towards a full spec.

2. Yes, you can refine later, but if you want to refine later (and in practise you almost always have the full spec -- if it exists at all -- only at the end), then why pay the cost of dependent types from the start? Once you have the full spec, verify with Hoare logic.

3, 4: I'm not sufficiently familiar with Idris to comment.

5. Alternative approaches, in addition owhat "pron" mentioned includes program logic, e.g. TLA.

[hope-striker]

1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.

[9q9]

This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.