The question that I am pondering is whether I can bridge the two by adding type-safe casting operations to the definitions of types. Perhaps by using some form of type-class, or concept.

Consider the following function grow_list which takes a list and appends an element to it a specified number of times:

define grow_list : (a:list x:value n:uint) -> (b:list)
{
  [[dup [append] dip] dip dec] [dup neqz] while pop pop
}

If the implementation is meaningless to you, it isn't very important, but it is pretty much the same as Joy.

The question is, should I express the postcondition as part of the type expression? The postcondition can be expressed in pseudo-code:

[{ b size } { a size n + } eq]

1. should the type system capture postconditions and other constraints
2. if so then what should the mechanism be for expressing constraints?

define grow_list : (a:list x:any n:int)->(b:list) 
  <: [{ b size } { a size n + } eq]
{
   ...
}

1    int fact(int n : n >= 0) {
2        int result;
3
4        if (n == 0) {
5            result = 1;
6        }
7        else {
8            int n1 = n - 1;
9            int f = fact(n1);
10           result = n * f;
11       }
12       return result; 
13   }

Line Input                   Output           
------------------------------------------
1    n(int)                  n(0 | pos int)   
4    n(0 | pos int)          n(0)
5    n(0)                    result(1)
8    n(pos int)              n1(0..n-1)
9    n1(0..n-1)              f(pos int)
10   n(pos int), f(pos int)  result(pos int)
12   result(1, pos int)      result(pos int)

  Fixpoint fact (n: nat): nat :=
    match n with
    | 0 => 1
    | S m => (fact m) * n
    end.

  Lemma fact_result: forall n, (fact n) > 0.
    unfold gt.
    induction n.
      simpl.
      apply lt_n_Sn.
    simpl.
    replace 0 with (0 * fact n).
      replace (fact n * S n) with (S n * fact n).
        apply mult_lt_compat_r.
          apply lt_O_Sn.
        assumption.
      rewrite mult_comm.
      reflexivity.
    reflexivity.
  Qed.  

  Lemma one_gt_zero: 1 > 0.
    unfold gt.
    apply lt_n_Sn.
  Qed.
  
  Lemma rec_call_valid (rec_val n: nat) (rec_spec: rec_val > 0): (rec_val * S n) > 0.
    unfold gt.
    intros.
    rewrite mult_comm.
    replace 0 with (0 * rec_val).
      apply mult_lt_compat_r.
        apply lt_O_Sn.
      assumption.
    reflexivity.
  Qed.
  
  Fixpoint fact_strong (n: nat): { r: nat | r > 0 } :=
    match n with
    | 0 => exist _ 1 one_gt_zero
    | S m => let (rec_val, rec_spec) := (fact_strong m) in
        exist _ (rec_val * (S n)) (rec_call_valid _ _ rec_spec)
    end.

template<typename T> locked
{
  T& locked_info;
 
public:
  locked(T& data) : locked_info(data)
  { /* yes, I'm locking *after* I've initialized, but before use; it's safe because I won't get that lock (and won't use the data) until any other locks on this data have been released -- meaning the data *should be* updated properly at that time. */
    lock(locked_info);
  };
 
  operator T&()
  {
    return locked_info;
  };
 
  ~locked()
  {
    unlock(locked_info);
  };
};
 
int add_two_locked(locked<int> x)
{
  return x += 2;
};
 
int main()
{
  int y = 3;
  add_two_locked(y);
};

map(fn,x:list) = cons(fn(car(x)), map(fn, cdr(x)))
map(fn,nil) = nil

length(x:list) = length(cdr(x)) + 1
length(nil) = 0

; counts the leaves of a tree
; count-leaves('(2 3 (5 5) 4)) => 5
 
count-leaves(x:pair) = count-leaves(car(x)) + count-leaves(cdr(x))
count-leaves(nil) = 0
count-leaves(x:any) = 1

> ; counts the leaves of a tree
> ; count-leaves('(2 3 (5 5) 4)) => 5
> 
> count-leaves(x:pair) = count-leaves(car(x)) +
> count-leaves(cdr(x))
> count-leaves(nil) = 0
> count-leaves(x:any) = 1

int count_leaves(l) {
    ensure(l does not belong in set of values referenced by l);
    if (l == null) return 0;
    if (l is not a list) return 1;
    return count_leaves(l) + count_leaves(next(l));
}

1 List l = new List;
2 append(l, l);
3 int c = count_leaves(l);