20
$\begingroup$

Many proof assistants start with the notion of $Type : Type$ which is inconsistent. This choice makes type checking and some natural recursions arguably easier. Of course, universe levels can be added on afterward, but I'm curious if any proof assistants have taken a different path by adding a notion of unsafety.

In the Rust programming language, there is an unsafe fragment that relaxes some of the restrictions of the full language. Some of those "superpowers" include:

  1. Dereference of a raw pointer
  2. Call other unsafe functions

Critically, safe interfaces can be constructed from unsafe components, with the implicit assumption that invariants required by safe code are enforced by the programmer (instead of the type/borrow checker).

The trusted computing base (TCB) of a proof assistant is generally considered a desirable thing to keep small (Coq and Isabelle for instance have reasonably small TCB, in my opinion). With unsafety, any unsafe portions of library or application code (or proof code!) would also be part of the TCB, at least in terms of making sure the invariants/properties that are used in the unsafe code are true. However, this is not an obviously bad situation because the core type checker could become much simpler if unsafety is designed as a feature from the beginning. Moreover, many different type systems could be shallowly embedded by directly using unsafety to build safe interfaces. As an example, many different variants of universe hierarchies could be implemented directly from unsafe recursive types and other standard safe features. Likewise, many flavors of safe recursive types can also be derived from unsafe recursive types by requiring monotonicity proofs as guards.

This is how I imagine such a proof assistant might look: Suppose we have only the combinators $Y, S, K, I$ with $S, K, I$ typed in any consistent way (such that $Y$ is not derivable from them). Then, we mark $Y$ as unsafe and require that any safe combinator, $C$, constructed using $Y$ must satisfy the invariant that using $C$ to construct any other safe combinator is still safe (Ideally, we want a local invariant to make this situation more reasonable to prove). Now, the definition of $C$ is part of the TCB, but any usage of $C$ is not.

Have any proof assistants taken an approach like this or similar?

$\endgroup$
9
  • 2
    $\begingroup$ Agda has an coinfective --safe flag an so on. But these flags only have file-wise granuality. I don't see any theoretical difficulties extending it to a per-declaration flag. $\endgroup$
    – Trebor
    Commented Feb 10, 2022 at 16:33
  • 2
    $\begingroup$ Lean is both a programming language and a theorem prover. The programming language part has safe and unsafe versions. In Lean3 code prefixed with meta can be partial (via unbounded recursion), have IO (via the IO monad or similar). It is typically used for metaprogramming like writing tactics. Lean 4 (which is a professional programming language similar in spirit to maybe Haskell and Agda) also has support for both safe and unsafe code. Also Lean 4 has support for replacing some code with faster FFI implementations or faster Lean versions of the same function. This is also unsafe. $\endgroup$
    – Jason Rute
    Commented Feb 10, 2022 at 18:56
  • 2
    $\begingroup$ Idris has per-declaration totality flags that let you mark e.g. nonstructural recursion or noncovering functions idris2.readthedocs.io/en/latest/tutorial/… and I'm pretty sure it'll infect other declarations in the way you describe (along with disallowing evaluating them during type checking), but it doesn't apply to uses of type-in-type (although that's because afaik Idris still has Type: Type atm...). $\endgroup$
    – ionchy
    Commented Feb 10, 2022 at 21:40
  • 5
    $\begingroup$ Freek Wiedijk once told me that Type in Type was his favourite system for formalising mathematics. "Who cares that it's inconsistent -- just don't do anything stupid". $\endgroup$ Commented Feb 11, 2022 at 6:47
  • 1
    $\begingroup$ Simple answer is: most. $\endgroup$ Commented Feb 11, 2022 at 23:42

1 Answer 1

8
$\begingroup$

I will summarize the answers from the comments and add my own about Coq.

Many proof assistants have a way of adding "unsafe" declarations and tracking which definitions rely on them.

  • Coq has Unset Universe Checking (a local version of the -type-in-type command-line option), which I believe is used, for example, by UniMath to introduce a computational resizing axiom. I believe Print Assumptions tracks whether or not a definition depends on use of this flag
  • Agda has the infective --type-in-type and the coinfective --safe flags, on a per-file granularity
  • Lean has the meta keyword for unrestricted recursion
  • Idris has per-definition totality flags
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.