u/azzqwa

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?