Comment by gz09

Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus?

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.

in case anyone's interested i have a vibe coded fork of verus that replaces the verus-the-language side of verus with plain old Lean 4. It's still two languages, but now at least the second language is as mainstream as it gets in the field and has good automation. i haven't finished wiring up the Lean 4 infoview and vs code extensions and LLM skills into it yet, which makes it not as easy to write yet as lean 4 with the IDE bells and whistles.

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.

Focus on formal verification is a technique to "harden" an unreliable LLM that produces meaningless slop from arbitrary text into a compiler that produces a correct program from a concise, formal input.

"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.

I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally verify a Rust-like borrow checker and at this point I have a working interpreter and LLVM compiler and a formally verified kernel.

All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.

This is the fantasy that has always driven proof systems research. Nobody is going to run software that has never been tested. Would ride a rollercoaster that had never actually been tested before, only "proven" safe? I wouldn't!

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.