Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
Versus appears to just be a formal verification tool. Perhaps I misunderstand?
You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages.
You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens.
The actual programming language and the verification language can be the same language though, if we want.
I'm also playing around with using the lean's compile-to-C tooling to instead compile to rust instead and it's getting more of my focus than the lean-via-verus route right now.
if people are interested, ping me and i can put them up on gh.
All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.
"Writing formal specs" means simply programming, taking a step upward in programming language abstraction level, and whether it's going to be easy remains to be seen.
So this stuff is always going to be additive and concerned with edge cases, as almost by definition, stuff that isn't edge cases will be found by comprehensive enough testing procedures.
And yet most software doesn't really need to be correct under edge cases, outside of security and data loss issues. People can tolerate a lot of incorrectness in other areas because it's just annoying, not critical.
Security is a case where formal methods could help, but I don't think LLMs will change the industries lack of interest. If anything it'll reduce it even further. Historically security took place in a fog of war. You don't know your enemies capabilities and may not be able to easily match them. But now LLMs are better at finding security bugs than most (all?) humans and ~everyone has access to them, so, from a liability perspective, all you have to do is point a frontier LLM at your codebase and let it fix as many bugs as it can find. Your enemies don't have access to anything better, so once it's done you can tick the box and say security is good enough. Meaning, nobody will fire you if there are still attacks possible.
So in the end I don't see LLMs changing the adoption formal methods.