Email Gateway (Aug 19 2022 at 09:10): Email Gateway (Aug 19 2022 at 09:10):From: Jens Doll <jd@cococo.de>
Hello all.
let me again ask a question about Isabelle proofs in common. Being a formal
language professional I wonder why these artefacts in your proof libraries
need the abstract language level at all. In my opinion most of the proofs
could be specified in context free syntax with the semantics attached to
it or having semantics in mind or specified elsewhere. If we had the proofs in
a CH(2) pattern we could build transformers to transfer them to and from other
formalisms, which in turn would foster exchange with other groups building
proof libraries worldwide. Am I wrong or is there a reason for maintaining
such a hurdle?
Happy reasoning,
Jens
<http://cococo.de>
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
Ancient LCF tradition already started this "syntax-less" attitude: it is
all just "semantics" (in ML) with some notation to produce it, and it is
extensible in all directions.
The Isar framework emphasizes this further, allowing the user (or rather
tool implementor) to invent new languages and embed them into the system.
Even the core proof language does not have fixed syntax, although there is
a reconstruction of some of it in appendix A of the isar-ref manual. This
integration of many languages is actually more close to common practice in
the world out there: consider "HTML5" and its many sub-languages that are
not HTML at all.
Makarius
Email Gateway (Aug 19 2022 at 09:13):From: Jens Doll <jd@cococo.de>
Do you have statistical data about language usage in the Isabelle
libraries known? A common ground exists at least on the Ch(3) level. My
personal experience also tells me that there is a Ch(2) basic language.
The idea of flexibility is understandable, but is similar to domain
specific languages, which might/should (deliberately) lead to Babylon
in commercial application development.
Jens
Last updated: Nov 21 2024 at 12:39 UTC