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:
- Dereference of a raw pointer
- 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?
--safeflag 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$metacan 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$