0
$\begingroup$

After receiving responses from this question as a Liberal Artist I'm interesting in other Proof Assistant appliances, beyond Mathematics and Software Verification. I was wondering: how one can use proof assistants in roles that don't imply mathematics directly but only after some level of rigour and subtle observation at necessary scale but different from Math top-level domain.

What I'm looking for could be:

  • Philosophy
  • Music
  • Chemistry
  • Physics
  • Biology
  • Natural Language Processing
  • Poetry
  • etc...
Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ I guess only Math, Logic Teacher would fit from this list. Maybe Formal Philosopher or Musician who want to deal with Music at Abstract Algebra level with Groups also could be added. There also is a generalization of proving of Web Development to Verification of Software. Anyway you should consult how to correct the Answer. The simple answer you can't use Proof Assistants without Math. $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 19:12
  • $\begingroup$ Or you can allow me to rewrite you question if you trustMe, seems I got your idea and can evolve the question for mathematicians. $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 19:32
  • $\begingroup$ @NamdakTönpa sure, I don't mind if you re-write :) $\endgroup$
    – taylor.2317
    Commented Feb 11, 2022 at 21:43
  • $\begingroup$ Check this out! Unfortunately I formulated question in a way we miss good answer from Dima. $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 21:54
  • 1
    $\begingroup$ If you will save this question from deletion I promise to answer! $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 22:04

1 Answer 1

Reset to default
6
$\begingroup$

They are used a lot in software development,to verify correctness of implementations, and even to generate executable code (this is called program extraction). See https://softwarefoundations.cis.upenn.edu/

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ I propose to put this answer into mentioned question "Proof Assistant Appliances" #6, where we already have curated list of Software Verification research. $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 22:19
  • $\begingroup$ You will miss acceptance but I will give you +10! :-) $\endgroup$
    – Namdak Tönpa
    Commented Feb 11, 2022 at 22:20
  • 1
    $\begingroup$ done, see proofassistants.stackexchange.com/a/414/74 (with few extras added) $\endgroup$
    – Dima Pasechnik
    Commented Feb 12, 2022 at 11:26
  • $\begingroup$ Great, thank you! $\endgroup$
    – Namdak Tönpa
    Commented Feb 12, 2022 at 12:57

Not the answer you're looking for? Browse other questions tagged or ask your own question.