Re: Why not Coq2Ada program extraction?

["Dan'l Miller" <optikos@verizon.net>]

On Sunday, May 6, 2018 at 11:20:23 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Here is an intro to the somewhat analogous codegen from HOL4:
> > https://isabelle.in.tum.de/doc/codegen.pdf
> 
> Thanks, that is interesting.  I've heard of Isabelle/HOL being used for
> verification in connection with Ada, but hadn't looked at it closely and
> thought it worked somewhat differently.

Isabelle is based on type inhabitation of various systems of logic into a generic kernel weak-type-theory system (an interface of sorts, if you will) in which various stronger systems of logic can be written (or plugged in, if you will).
https://en.wikipedia.org/wiki/Logical_framework

from https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
“Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like first-order logic (FOL), higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.”