10
$\begingroup$

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)?

$\endgroup$

1 Answer 1

15
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ That Lean 4 feature is interesting, but it doesn't have a while loop, right? I guess so because otherwise you can't guarantee that the function to be defined is terminating, at least easily. Also I heard of Why3 before but didn't really look into it - great one, but not a perfect fit for my question since I can't use the function defined that way to specify other theorems. $\endgroup$
    – Bubbler
    Feb 10, 2022 at 23:40
  • $\begingroup$ "in an imperative language these (writing programs and writing proofs) necessarily diverge" - Can you elaborate further? "Dependent type theory is one way to unify..." I get this part, but is there a specific reason why they can't be in an imperative language? How about an imperative language that supports dependent types? $\endgroup$
    – Bubbler
    Feb 10, 2022 at 23:45
  • $\begingroup$ @Bubbler You have to write while loops with recursion, but you can write nonterminating loops if you use the partial keyword, or you can prove termination (it does not have to be structurally terminating). $\endgroup$ Feb 11, 2022 at 1:56
  • 1
    $\begingroup$ "How about an imperative language that supports dependent types?" The question is: what is the grammar that you can use in the specification part of the language? For example if you have a sorting function with a comparator input, you would like to say that the result of the function is sorted, but this would require calling the comparator in the specification. If that comparator does something non-pure then it's really unclear what the meaning of that specification is, since it seems to change every time you query it. $\endgroup$ Feb 11, 2022 at 1:59
  • $\begingroup$ There are of course ways to answer the question (full disclosure: I'm working on one myself), but you generally need "purity" to be a first class notion in the language and distinguish between the pure functions that can appear in specifications and the impure functions which can be subject to specification but cannot otherwise be referenced directly in logical propositions. $\endgroup$ Feb 11, 2022 at 2:01

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.