D>>Мечта — это чтобы программы сами писались?

D>>data OList : Nat -> Set where 
D>>  Nil  : {b : Nat} -> OList b 
D>>  Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
D>>

data Nat : Set where
 zero : Nat
 suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
 zero  + m = m
 suc n + m = suc (n + m)

data List (a : Set) : Set where
 []   : List a 
 _::_ : a -> List a -> List a

data List (a : Set) : Nat -> Set where
 []   : List a zero
 _::_ : {n : Nat} -> a -> List a n -> List a (suc n)

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

I've come up with a set of rules that describe our reactions to technologies:
1. Anything that is in the world when you're born is normal and ordinary and is just a natural part of the way the world works.
2. Anything that's invented between when you're fifteen and thirty-five is new and exciting and revolutionary and you can probably get a career in it.
3. Anything invented after you're thirty-five is against the natural order of things.
— Douglas Adams

listA = getListA (void -> Vec A n)
listB = getListB (void -> Vec B n)

zip listA listB // как тут компилятор понимает какой длинны listA и listB

do
  listA <- getListA : IO (Vec A n) //побочные эффекты в IO
  listB <- getListB : IO (Vec B n) //

  ... zip listA listB ... // и что-то с этим результатом будем ещё делать

IO {exists n}(Vec A n)
IO {exists n}(Vec B n)

zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))

VD>>>zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
VD>>>

VD>>>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>>>  requires l1.Lenght == l2.Lenght
VD>>>  ensures  value.Lenght == l1.Lenght
VD>>>

VD>Ну, что же. Можешь радоваться, так как ты вместе с еще 3 человеками сможешь в этом во всем разбираться.

WH>>zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n
WH>>

VD>zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]
VD>

zip[A : Type, B : Type, len : int](l1 : list(A, len), l2 : list(B, len)) : list(A * B, len)

VD>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>  types invariant l1.Lenght = l2.Lenght = result.Lenght
VD>{
VD>  ...
VD>}
VD>

l1.Length == l2.Length, l1.Length == result.Length

GetData[int, n : int]() : list[int, n]

GetData() : (n : int) * list(int, n)

Zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]

VD>def res = Zip(GetData(), GetData());
VD>WriteLine(res);
VD>

def res : list[int * int, 0] = Zip[int, int, 0](GetData[0](), GetData[0]());
WriteLine(res);

def (n,data1) = GetData(); // data1 : list(int, n)
def (m,data2) = GetData(); // data2 : list(int, m)
def res = Zip(GetData(), GetData());
WriteLine(res);

1. Выдать исключение.
2. Отбросить "лишние" элементы из более длинного списка.

Zip1[A : Type, B : Type, n : int, m : int](l1 : list[A, n], l2 : list[B, m])
{
  def k = min(n, m);
  def l1' = Take(l1, k);
  def l2' = Take(l2, k);
  return Zip(l1', l2');
}

Main() : void
{
  def (_,data1) = GetData();
  def (_,data2) = GetData();
  def res = Zip1(GetData(), GetData());
  WriteLine(res);
}

sum x:int y:int — хочется Х (Х — спецификация оператора +)

sum x:int y:int — хочется Х (Х — спецификация оператора -)

WH>zip : forall{A B n} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
WH>

WH>zip []    []    = []
WH>zip x::xs y::ys = (x, y) :: zip xs ys
WH>

WH>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
WH>

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
  requires l1.Lenght == l2.Lenght
  ensures  value.Lenght == l1.Lenght

WH>{
WH>| ([],    [])    => []
WH>| (x::xs, y::ys) => (x, y) :: zip(xs, ys)
WH>| _              => throw InvalidArgumentException()
WH>}
WH>

zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
  requires l1.Lenght == l2.Lenght
  ensures  value.Lenght == l1.Lenght

VD>>Ну, а то что мы тут увидели вряд ли можно назвать простым.

listA = getListA (void -> Vec A n) //читает список из файла listA.txt
listB = getListB (void -> Vec B n) //читает список из файла listB.txt

zip listA listB // как тут компилятор понимает какой длинны listA и listB

lameZip : {n m : Nat}{A B : Set} -> (v1 : Vec A n) -> (v2 : Vec B m) -> Vec (A, B) n
lameZip = zip v1 (v2 :> Vec B n)

def test(x):
    requires(x > 0)

test(-10)

WH>data Vec (A : Set) : Nat -> Set where
WH>  [] : Vec A zero
WH>  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
WH>

template <int v>
struct Int2Type
{
   enum { value = v; }
}

zip : forall{A B n} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

zip []    []    = []
zip x::xs y::ys = (x, y) :: zip xs ys

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]

{
| ([],    [])    => []
| (x::xs, y::ys) => (x, y) :: zip(xs, ys)
| _              => throw InvalidArgumentException()
}

data OList : Nat -> Set where 
  Nil  : {b : Nat} -> OList b 
  Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b

sort : List Nat -> OList 0

sum x y = x + y

D>>>Мечта — это чтобы программы сами писались?

D>>>data OList : Nat -> Set where 
D>>>  Nil  : {b : Nat} -> OList b 
D>>>  Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
D>>>

D>>>sort : List Nat -> OList 0
D>>>

sort : List Nat -> OList 0
otherFunc : List Nat -> не_важно_что

sum x y = x - y

sum x y = x + y

SH>>>>>Я только про то, что "доказать, что нет багов" невозможно концептуально, вне зависимости от языков, средств и т.п.
D>>>>Даже для
D>>>>

D>>>>sum x y = x + y
D>>>>

D>>>>?

А>>>А если в спецификации было написано "реализовать функцию вычитания целых чисел с именем sub"?
D>>Не уловил подвох.

А>Подвох в том, что глядя даже на такую простую штуку как
А>

А>sum x y = x + y
А>

А>нельзя сказать есть в коде бага или нет.

VD>zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
VD>

VD>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>  requires l1.Lenght == l2.Lenght
VD>  ensures  value.Lenght == l1.Lenght
VD>

zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n

VD>Я не заметил чего-то выносящего мозг. Видимо по второму разу данная трава уже не так выносит .

listA = getListA (void -> Vec A n)
listB = getListB (void -> Vec B n)

zip listA listB // как тут компилятор понимает какой длинны listA и listB

VD>>zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
VD>>

VD>>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>>  requires l1.Lenght == l2.Lenght
VD>>  ensures  value.Lenght == l1.Lenght
VD>>

WH>zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n
WH>

zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
  types invariant l1.Lenght = l2.Lenght = result.Lenght
{
  ...
}

VD>>Я не заметил чего-то выносящего мозг. Видимо по второму разу данная трава уже не так выносит .

GetData[int, n : int]() : list[int, n]

Zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]

def res = Zip(GetData(), GetData());
WriteLine(res);