I have been playing around with an idea for a programming language that enables practical theorem proving.

The core idea behind it is that statically proven assertions would be really powerful.

Loop invariants can be simply expressed as an assertion inside the loop.

Additionally, to give it a bit more power; assertions could be given the ability to act over sets (say over all ints).

This might look something like

  XY = {int, int}

  @assert commutative
  fn add(a XY, b XY) XY {
    return (a[0]+b[0], a[1] + b[1])
  }
  
  fn commutative<a,b>(f (a,a)b){
    assert x,y: f(x,y) == f(y,x)
  }

And then it would also be helpful to add on assertions to types so assignments to variables also checks the assertions

  order = enum {greater, equal, lesser}
  comparator<a> = (a,a)order
  
  fn sorted<a>(pair ([]a,comparator<a>))bool {
    (l, cmp) = pair
    if l.length() <= 1 {
      return true
    }
    return cmp(l[0],l[1]) != order.greater & sorted((l[1:],cmp))
  }
  
  SortedList<a> = ([]a,(a,a)order) & sorted

There are a few major issues with my idea currently (it really requires dependent types to be ergonomic and allocation and pointers could be strange) which have prevented me from making a quick demo compiler or language spec. But I would be very excited to discuss it.