5 ms·
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
by Buttons840 2mo ago
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.
- trenchgun 2mo agoLean4 is a general purpose programming language.
- singularity2001 2mo agoHave you tried writing any programs in it?
- ndriscoll 2mo agoI 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.
- trenchgun 1mo agoI 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.
- kachnuv_ocasek 2mo agoHaskell does not have dependent types.
- tsimionescu 2mo agoDepends what you mean by "Haskell". There is at least one dependent types extension for base Haskell.