Any proof assistant that allows imperative computation within the language itself?

Question

To my knowledge, the well-known ones like Coq, Agda, Lean are all purely functional languages, and therefore require any computational function to be written in lambda calculus style. For example, you cannot directly write down an imperative algorithm for isprime: nat -> bool equivalent to, say, a C-like function

bool isprime(nat n) {
    if n < 2 {
        return false;
    }
    for i in 2 to n-1 {
        if n % i == 0 {
            return false;
        }
    }
    return true;
}

Instead, Coq/Agda/Lean requires the computation to be written in functional style, or you need to encode the computational model itself and reason about the process of computation manually (e.g. via modeling state transition as a binary relation and reasoning about its reflexive transitive closure).

Is there any proof assistant implementation that allows imperative computation? Is it at least theoretically possible? What are the main challenges to allowing it (if any)?

Answer 1

Although Lean 4 is a pure functional programming language, it is capable of expressing functions almost exactly like your example:

def isprime (n : Nat) : Bool := Id.run do
  if n < 2 then
    return false
  for i in [2:n-1] do
    if n % i == 0 then
      return false
  return true

But you can argue that this is a cheat, since really lean is a functional language at heart, and this is true. What about "truly imperative" languages? Well, one issue with non-pure-functional languages is that functions are not pure, which means that you have to be careful about using them in specifications. What does the proof language even look like? Dependent type theory is one way to unify the concept of "writing programs" and "writing proofs"; in an imperative language these necessarily diverge.

It is, of course, possible to prove properties of imperative programs, but these tend to take the form of annotations around code, either using refinement types or design by contract style requires and ensures clauses around functions, loop invariants and other critical points in the code, with some automation to fill in the gaps. Why3 and Dafny are two strong examples of languages designed for reasoning about imperative code.

Another interpretation of your header question is "a proof assistant that does imperative computation in the course of proving theorems", and I think there are plenty of examples of this, because the metalanguage of a scriptable proof assistant can be any language at all. Isabelle and the HOL family use ML or OCaml as their metalanguage, which is not a pure functional language (although it has lots of functional leanings). Metamath is a proof language primarily used for proving theorems in ZFC, and the mmj2 proof assistant for it (written in Java) allows running user tactics written in Javascript, which is not really a functional language. Generally, I would say that there is no need for a functional language in this space, but rather the people working in the space have a predisposition toward functional languages, either because they are easily embeddable or because functional features are good for writing operations on syntax.