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.
I did write small programs myself, but mostly with Claude Code. It was very pleasant to work in it with Claude Code. Implemented a shell and 40 of coreutils. Did not really get very far with proving properties of them, but had working programs. Reading Lean4 is pretty nice. Nicer to read than OCaml, almost as nice as Haskell.
I don't see why it would be particularly difficult beyond not already having a lot of IO libraries (like Kafka connectors or whatever). Pure functional programming in Scala with IO monads is quite pleasant.
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.