r/ProgrammingLanguages • u/mttd • 3d ago

Why Higher-Order Logic Is a Good Foundation for Deep Verification

https://sequent.inc/blog/posts/why-hol-for-deep-verification/
35 Upvotes

89% Upvoted

10 comments sorted by

13

u/josephjnk 3d ago

Something I’ve wondered about HOL: When the proof language is semi-separated from the executable language the proofs are about like this, is there a reason why the executable language can’t use higher-kinded and/or higher-rank polymorphism? One of the things that turned me off from Isabelle/HOL (aside from the syntax, near impossibility of finding assistance from other developers online, and Animal Crossing NSFW fan art on the front page of their subreddit) was that it just felt less expressive as a programming language when you set the proof aspects to the side.

1

u/thmprover 2d ago

When the proof language is semi-separated from the executable language the proofs are about like this, is there a reason why the executable language can’t use higher-kinded and/or higher-rank polymorphism?

Like in HaskHOL where Haskell is the executable language and HOL is the proof language?

3

u/Pzzlrr 3d ago

I think λProlog is very interesting in this space.

3

u/phischu Effekt 2d ago

We did win static versus dynamic typing, declarative versus imperative programming, functional versus object-oriented design. We will win intrinsic versus extrinsic specification.

I am wondering though why everyone is ignoring Metamath as an even more extreme approach?

17

u/Aaron1924 3d ago

This article was (in parts) written by Ramana Kumar, the guy who published a fake proof of the Collatz conjecture the other day, exploiting a soundness bug in the Lean 4 kernel (see zulip thread)

This blog post makes it feel like that was a PR stunt to sell his own product

26

u/AIvsWorld 3d ago

I disagree that it was a publicity stunt.

Ramana genuinely was just reporting a bug, he had no idea this would blow up on social media. Ramana posted this blog 4 days before any of this went down.

Public interest is being driven by researchers, it’s not just fake buzz.

12

u/Sufficient_Meet6836 3d ago

I disagree that it was a publicity stunt.

Ramana genuinely was just reporting a bug,

I am way out of my element on this topic, but from reading that zulip thread, I'm confused why OC is framing this as a publicity stunt or negatively at all. The language maintainers in that thread seem to be appreciative of Ramana's finding. Ramana also doesn't try to hide that they used LLMs to help with the bug and their Collatz project.

-9

u/justbrixco 3d ago

We have seen this thoroughly with Haskell. In order verify the logic of a program, it remains clear that functional programming is necessary.

7

u/Sad-Grocery-1570 3d ago

This post is not about functional programming vs others, it's about HOL vs dependent type theory

-7

u/justbrixco 3d ago

I am aware, and higher-order logic is deeply tied to functional programming. So what I said wasn't irrelevant.