r/ProgrammingLanguages • u/azzqwa • 16d 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?

14 Upvotes

94% Upvoted

16 comments sorted by

View all comments

Show parent comments

2

u/Clifspeare 13d ago edited 13d ago

Heavily agree. I've used Rocq heavily for years but Lean is so much more pleasant than the cobbled patchwork of opam/dune plugins that Rocq needs, so I've switched completely despite being initially hesitant.

I've also heard F* is pleasant to use, but Lean has a lot of momentum at the moment and network effects are also a thing.

2

u/InviteQueasy3739 13d ago

I absolutely despise Lean 4, but I have to admit that using Rocq causes me physical pain. Every time, I find myself cursing that ecosystem. Meanwhile, Lean 4 sounds as pleasant as Rust to me. Everything just works™.

I wish I had the skills to write my own, completely opinionated proof assistant.

2

u/EatThatPotato 11d ago

What are your issues with lean? It’s my first proof assistant so I have no reference point

1

u/InviteQueasy3739 11d ago edited 11d ago

It's no big deal, really. I just don't really like how the language is so heavily geared toward integration with code editors, and that its core is written in a language that isn't particularly memory-safe.

I know it's a language that has been extensively researched, with countless papers and significant contributions (Perceus, for example), but I have this little issue with Lean 4.

Edit: Perceus was actually developed for Koka.