alt Hacker NewsStrongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done.
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).
Replies
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.
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.