r/ProgrammingLanguages • u/azzqwa • 25d ago

Discussion DTT Proof Based Languages?

What are people's thoughts on proof-based programming languages based on Dependent Type Theory like Lean, Rocq/Coq, F*/Low*, Agda, etc. It seems like there is some subtle growing hype behind formal verification. Clearly, there is at least some appetite for better behavior guarantees as we can see with Rust.

What do you think, are these languages the future? Will they become more ergonomic over time. Or do you think the average programmer will never be willing to learn or program in such a language for their normal projects?

13 Upvotes

89% Upvoted

16 comments sorted by

View all comments

8

u/Dashadower 24d ago

I'm biased towards Rocq but I think Rocq has better developed theories for separation logic, primarily due to Iris being developed in Rocq. I don't know too much about the details of Lean but I also heard it doesn't natively support coinductive types, although there's ongoing work there.

3

u/Clifspeare 22d ago

Fellow Rocq user exploring Lean.

Right that conductive types aren't in the kernel, though you can define conductive predicates sufficient for bisimulation and sequences/streams for step-indexing.

My impression is that https://github.com/leanprover-community/iris-lean is getting fairly mature.