Proof-based language

exists.

property transitive {
  let r(a) : Relation on a.
  let x, y, z : in r.
  assume (x, y) in r.
  assume (y, z) in r.
  declare (x, z) in r.
}

hello.txt

law DeMorgan {
  let a : Bool.
  let b : Bool.
  declare ~(a | b) == (~a & ~b).
}

proof main proves ~(x | y) {
  val x = True.
  val y = True.
  val z = print(~(x | y)).
}

set.txt

property symmetric {
  let r(a) : Relation on a.
  
  declare every a, b[
    if (a, b) in r
    then (b, a) in r
  ].
}

// Proofs can be anonymous.
proof proves if (a, b) in r then (a, b) in r^-1 {
  let r(a): Relation on a.
  let a, b : in r.
  assume (a, b) in r.
  (b, a) in r.
  (a, b) in r^-1.
}