4 ms·
1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature forall T. Array[T] -> (T -> T -> Bool) ->
by 9q9 7y ago
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 7y ago1. 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 7y agoThis 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.