2 ms·
Random passerby chiming in: so this means you can write "regular" software with this stuff? While reading TFA I thought the theorem stuff deserved its own cate
by andai 7mo ago
Random passerby chiming in: so this means you can write "regular" software with this stuff?
While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family?
It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
- nextaccountic 7mo agoYes Idris was meant to write regular code. F* is also meant to write regular code But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff. Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html https://kirancodes.me/posts/log-ocaml-to-lean.html
- Hendrikto 7mo ago> if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl! Does not sound that appealing to me. Sounds like little consistency and having to learn a new language for every project.