[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.