[tomsmeding]

This sounds to me like dependently-typed languages might fit the bill. Look at Agda (more fancy-features focused) or Idris (more real-world programming focused).

Their idea is that you can lift value-level computations to the type level one-to-one. This allows you to do tricks with them that are normally only reserved for type-level things: things like equality proofs that are verified at compile time. In fact, the main reason why dependently-typed languages are developed is to exploit the Curry-Howard correspondence saying that every first-order logic statement corresponds to a _type_ in a dependently-typed language, and the validity of the statement is equivalent to the existence of an inhabitant of that corresponding type (= a value that has that type). This allows you to prove arbitrary properties about the functions in your program without ever leaving your programming languages!

Maybe not exactly what you were looking for, but it technically fits your bill :)

[carnitine]

Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theories. System F, which is weaker than dependent type theory corresponds to higher-order logic. First-order logic actually doesn’t actually correspond to a popular type system, though the correspondence of course exists.