Proof-carrying Nim

transitive_implication.nim

# Hello world program

type
  Implies[A, B] = proc(a: A): B

# example Propositions
type
  X = object
  Y = object
  Z = object

proc transitive_implication(hypothesis_XY: Implies[X, Y],
                            hypothesis_YZ: Implies[Y, Z]): Implies[X, Z] =
  # if you are able to construct a value of the result type from the input types
  # you are proving that the result proposions follows from the hypotheses
  result =
    proc(x: X): Z =
      let y = hypothesis_XY(x)
      let z = hypothesis_YZ(y)
      return z

  # one problem is that in Nim it's possible cheat and produce the final type
  # without real construction:
  let problem =
    proc(x: X): Z =
      discard