Hacker News Reader

Comment by derefr | Hacker News Reader

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?

View on HN

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...

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.

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

> 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.

Would it be tenable to build a parameterized axiom-system-evaluation-engine for which the semantics of a specific proof-assistant would consist of a configuration for this general engine, rather than patches to its code?

If so, would it then be possible for interop to happen "between" proofs in slightly-different axiom systems, the way that regular hand-written "translational" proofs work in mathematics — i.e. "take this property we've proved, translate it into domain model X, derive a property Y, then translate property Y back out of domain model X and into domain-model Y, where we actually want to use it?" — but all under-the-covers, as the (proven) equivalent of FFI, autogenerated as glue proof-code by analyzing the differences between two "configurations" to the engine?

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.

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.

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.

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).

"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?

I think the closest thing in usage is Liquid Haskell. Although not a standard proof, the ‘refinement’ types serve as a linearly solvable language of predicates on types. The syntax is relatively standard (in the way of set comprehensions), but it is limited to a subset of what can be captured with ‘full spectrum’ dependent types.

I'm in the exact same boat. I've been playing with a domain checker for a restricted set of C for a kernel project, specifically for this reason.

But as of now I'm having to add better support for plugins in clang.

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...

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/

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

No, because System F cannot be used to express particularly interesting proofs.

Reply on news.ycombinator.com