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.

▲

kachnuv_ocasek 19 hours ago | parent | next [-]

Haskell does not have dependent types.

	▲	tsimionescu 18 hours ago \| parent [-]
		Depends what you mean by "Haskell". There is at least one dependent types extension for base Haskell.

▲

trenchgun 19 hours ago | parent | prev [-]

Lean4 is a general purpose programming language.

▲

singularity2001 17 hours ago | parent [-]

Have you tried writing any programs in it?

	▲	ndriscoll 4 hours ago \| parent [-]
		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.