Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order logic, set-theory, group-theory and so on).

To be useful as an archive it is important to be able to formulate the proof in a human-readable way which should be possible with the declarative proof languages (e.g. Czar for Coq and Isar for HOL/Isabelle).

But I haven't found a lot of material (especially proof examples) for both languages (Czar,Isar) and literature on the subject stops around 2005. Both languages seem to be somewhat abandoned (the declarative languages, not the proof assistants themselves).

Now my questions are:

• General questions on formalising math/logics:
  
  • Has anybody experience in formalizing math in a declarative way?
  • What are the limitations of this approach?
  • Are the resulting proofs digestible to the human reader without running the script in parallel (which is necessary e.g. for Coqs' tactics language)?
• Question concerning the integration status in proof assistants:
  What is their current status - are they deeply integrated into the systems and actively maintained? Or is this subject abandoned (if so, why)? I can't find any recent material on both Czar and Isar.
• Possible alternatives:
  Besides Coq/Czar, Isabelle/Isar and Mizar are there any other mature systems that allow for declarative proofs?

Thank you very much!

I am working in a version of ZFC set theory that attempts to formalize the notion of context used in mathematics textbooks at undergraduate and graduate level. It is named Contextual ZFC or CZFC. By trying to achieve this goal, I found myself working in three separate but very related lines:

1) Developing an implementation of CZFC, a language I named Mathdialog. It can be used to write definitions, theorems and proofs in a formal way using the associated system. This interaction it is named human-to-machine . Of course, to make this tasks the user must know the Mathdialog language, that is simply and very close to the language used in textbooks. However, once the system has those definitions, theorems, and proofs, the system is able to transform them in very natural versions, in particular, the proofs are showed in an interactive hypertext environment that resemble a teacher in a class willing to clarify many of the doubts the user can have. For this interaction, the user doesn't need to know anything about CZFC, but just a minimal mathematical background. This interaction is named machine-to-human. I encourage you to browse the content available right now, that is named the NUCLEUS, the minimal background Mathdialog needs to work.

2) In foundational terms, normally, set theory and ZFC in particular, is defined in the framework of predicate calculus, “the logic of quantification”, that in turn it is defined in the framework of propositional calculus. Instead, CZFC it is defined in the framework of propositional calculus and deals with quantification with its own internal rules that happen to be very intuitive and implicitly used in undergraduate and graduate mathematical textbooks.

3) From the philosophical point of view, CZFC is a computer evolution of the famous quote of David Hilbert: “Mathematics is a game played according to certain simple rules with meaningless marks on paper.” In the times of Hilbert, simple rules, means a deep detail like the one in 'Principia Mathematica' of Whitehead and Russell. It is my view such a level of detail is was necessary because the paper has zero information processing power. Today, they are not marks on paper but characters in computer memory, this should have let increase to decrease significantly the detail level by letting those details to the computer making formalization more natural. However, Proof Assistants like Coq, Mizar and Isabelle have had limited success to enter in the mathematical community. I can not enter into considering the reason of this.

In CZFC, I have abandoned some well-established paradigms. What may be adequate and acceptable, for a human being, to be the basis of an axiomatic system, may not be adequate for a computer. Instead of trying to turn proofs into programs, CZFC was guided by adapting the foundation of mathematics, originally developed to deal with marks on paper, to deal with characters in computer memory. In this task, I hold two principles, keeping formalization and keeping the essence of ZFC. Everything else I was ready to modify or abandon, even the minimalist aesthetic of accepted axiomatic systems. For instance, the set of Real number is a constant in CZFC almost in the same sense of the empty set.

Exist an implementation of CZFC that can be used right now in mathdialog.com to browse the NUCLEUS, notice that no background in CZFC or Mathdialog is needed.