(Replying to PARENT post)

To me, in terms of the expectations of modern programming, the weird thing about proof languages is that they’re languages in the first place.

AFAIK, a lot of proof-language code is machine-generated. And even when it isn’t, the syntax and semantics of these provers seem to be stuck in the era of “one runtime, one language”, where switching languages forces you to switch runtimes, and proof libraries written for different proof languages can’t be used together in the same project because they have different core runtime semantics.

Why isn’t there instead a “proof-checker VM” that accepts some formally-specced “proof bytecode” with a formally-specced standard semantics, that 1. is easy for machines to generate, and 2. where these different proof-languages would then be compilers emitting said bytecode?

👤derefr🕑4y🔼0🗨️0

(Replying to PARENT post)

Isabelle is a generic proof engine, can be combined with any fronted which satisfies its API (it’s a bit more complicated) so yes such thing exists.

Proof assistants aren’t whimsical like cottage industry of programming languages. Proof assistants are divided into 3 parts, the core or foundation (F) which is a very small language at the heart of the prover, the vernacular (V) the language in which humans write the code and the meta language for proof search and meta programming (M).

The V is translated into F and this translation is often proven to be correct. De Bruin criteria says that F has to be small and should be independently checked (mostly through inspection or mechanization in other framework). In Coq the proof derives is again checked from ground up by F when you write Qed.

Andrej Bauer explains better than I can.

https://mathoverflow.net/questions/376839/what-makes-depende...

👤sadfev🕑4y🔼0🗨️0

(Replying to PARENT post)

Idris works by compiling the language to a fully specified intermediate representation that the checker acts on. The IR is described in a well-written publication and could fulfill the role of your suggested general checker. However, since proof checkers are relatively easy to write, most of the work being in the standard library, people don't seem to mind remaking them every time they design a new language.

The biggest advantage would be gained from increased interoperability between dependently typed language so that they could use each other's standard libraries, but the field may not yet be well-developed enough to standardize on basic definitions.

👤whatshisface🕑4y🔼0🗨️0

(Replying to PARENT post)

That is basically the pitch for Metamath Zero[0].

I'm philosophically aligned with you. Basically, I think this is because of where resources are invested - there's a tremendous amount of work on programming languages to make them ergonomic and enable composition of pieces. Much of that work is at its essence processing friendly syntax into some form of typed lambda calculus. Since dependently typed lambda calculus is a very handy way to encode proofs, it's easier to just adapt that all that mechanism than to develop infrastructure just for proofs.

Interop is hard, because all the axiom systems tend to be subtly different in ways that are hard for normal people to appreciate, though there is some work on it, including MM0.

[0]: https://github.com/digama0/mm0

👤raphlinus🕑4y🔼0🗨️0

(Replying to PARENT post)

For the same reason that there isn't a universal ABI for normal programming languages, nobody can really agree on what the foundation should be and interoperability between different foundations is very hard.
👤ImprobableTruth🕑4y🔼0🗨️0

(Replying to PARENT post)

You're touching on something that's boosted the progress of languages with proof capabilities such as Spark and Frama-C. They standardized around the use of why3, and use it as a lever to harness state of the art SMT engines (z3, cvc4, alt-ergo) but also advanced specific provers on specific theories (floating point in particular, I'm thinking of gappa, the amazing work of the toccata lab, and Altran UK making incredible strides in the last 5 years). As soon as a new proving tool is plugged in why, you can harness it. And they built bridges for interactive proof with coq and Isabelle, but also with static analysis tools like codepeer.

Why3 is a big success in the way you're asking. Just not adapted to pure maths proof like lean.

👤touisteur🕑4y🔼0🗨️0

(Replying to PARENT post)

That's a great idea. Kind for example compiles to a small core language called FormCore which can be typechecked with 700 lines of javascript. In theory other languages could compile to FormCore and have good interoperability with Kind.
👤rigille🕑4y🔼0🗨️0

(Replying to PARENT post)

For the HOL family (HOL-light, HOL4, Isabelle/HOL) at least, there is such a VM: OpenTheory (http://opentheory.gilith.com/). It's a stack machine with a very simple input format (line based).
👤c-cube🕑4y🔼0🗨️0

(Replying to PARENT post)

"To me, in terms of the expectations of modern programming, the weird thing about proof languages is that they’re languages in the first place."

I've got a similar, but unrelated problem.

Most proof and formal methods languages development has involved dependently typed languages (modulo Frama-C and Spark). Which are dandy. However, the formula definitions are all in low-level, function-application-ish form, while the proof techniques are in high-level tactics. The result is that plain ol' simple formal logic is not directly applicable to using the formal techniques, and the proofs are completely unreadable.

Why aren't the formal techniques syntax-sugared into something understandable?

👤mcguire🕑4y🔼0🗨️0

(Replying to PARENT post)

I thought SMT2 (what you can feed to z3 -smt2), is a s-expression language that is the lowest level ("bytecode") thing. If you look at Dafny/Boogie, boogie is a much more human readable IR. I'm trying to build a pythonic variant of Boogie.

https://github.com/adsharma/py2many/blob/main/tests/cases/de...

👤adsharma🕑4y🔼0🗨️0

(Replying to PARENT post)

I think Kind-Core should be that language. It is the simplest proof kernel, after all, by far :) And it has nothing human or inventive. Basically just the lambda calculus with the self dependent function type. But I guess it ultimately is this old XKCD kind of problem: https://xkcd.com/927/
👤LangMakers🕑4y🔼0🗨️0

(Replying to PARENT post)

isn't system F (with some extensions) exactly this kind of VM? some functional languages (more or less) use (something like it) as the last functional intermediate language for compilation
👤valyagolev🕑4y🔼0🗨️0