Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A perfectable programming language

alok.github.io

Post reply on HN
Print view View original

81–90 of 152 posts

Re: A perfectable programming language

#81

Post by ux266478 »

harperlee wrote: post #80
codebje wrote: post #70

Earlier quoted context omitted.

The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that. Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity. I don't consider there to be a dependently typed language for writing programs that you just want to run, but I w…

I think Idris 2 is targeted more to programming than to doing math, no?

Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.

Re: A perfectable programming language

#82

Post by eggy »

landl0rd wrote: post #75
solomonb wrote: post #11

i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced. i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.

Imo F* is a much better choice for proof-oriented programming than lean4. The latter is still largely about mathematics while the former has things like https://fstarlang.github.io/lowstar/html/LowStar.html

Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.

Re: A perfectable programming language

#83

Post by addaon »

ux266478 wrote: post #81
harperlee wrote: post #80

Earlier quoted context omitted.

I think Idris 2 is targeted more to programming than to doing math, no?

Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.

Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.

Re: A perfectable programming language

#84

Post by nobleach »

tizzy wrote: post #64
nobleach wrote: post #59

The perfect programming language has: - The compile speed of Go - The performance of Go - The single binary compilation of Go - The type system of Kotlin - The ecosystem of JVM (packages for anything I could dream of) - The document sytem/tests of Elixir - The ability to go "unsafe" and opt for ARC instead of GC - The result monad/option monad and match statements from OCaml/Gleam - A REPL like Kotlin or even better,…

I believe there are tradeoffs which is why this doesn't exist. Isn't the compile speed of Go so good because it's type system is much simpler?

oh yeah absolutely. The moment you start blowing up Go with features (for example) the speed decreases dramatically.

Re: A perfectable programming language

#85

Post by unnouinceput »

nobleach wrote: post #59

The perfect programming language has: - The compile speed of Go - The performance of Go - The single binary compilation of Go - The type system of Kotlin - The ecosystem of JVM (packages for anything I could dream of) - The document sytem/tests of Elixir - The ability to go "unsafe" and opt for ARC instead of GC - The result monad/option monad and match statements from OCaml/Gleam - A REPL like Kotlin or even better,…

"The compile speed of Go" - Delphi starts laughing

Re: A perfectable programming language

#86

Post by nobleach »

ModernMech wrote: post #72
tizzy wrote: post #64

Earlier quoted context omitted.

I believe there are tradeoffs which is why this doesn't exist. Isn't the compile speed of Go so good because it's type system is much simpler?

Yes, programming languages are designed for a purpose and importantly for a concrete system. Erlang is the way it is because it was designed for Ericsson's phone network. C is the way it is because it was designed for the PDP-11. Logo is the way it is because is was designed for young children. Go is they way it is because it was designed by Google for Googlers. You can't design an abstractly "perfect" programming la…

No, I realize that. It doesn't stop me from having my "perfect language wishlist". The author calling out "perfectable" is what got me thinking. What language would I choose if I were able to "perfect" it just a bit more?

Re: A perfectable programming language

#87

Post by iLemming »

harperlee wrote: post #66
kleiba2 wrote: post #40

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean. Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.

The question then is how they plan to avoid The Lisp Curse (in my words, language giving you too much power makes you do weird things, and you attract people to like to use things a tad too powerful / generic, and you end up with an unproductive culture).

> you end up with an unproductive culture

Practical Lispers would like to have a word - I've been witnessing extreme productivity on some teams.

Modern Lisp dialects (Clojure and likes) largely broke library fragmentation and the "not invented here" tendency that were causing real tensions in Common Lisp.

You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion.

You can take it word-by-word and apply to say Javascript, and it would largely feel true - JS arguably has the worst fragmentation of any ecosystem; dozens of competing frameworks, build tools, bundlers, test runners; new frameworks constantly replacing old ones; "Javascript fatigue" is a real thing, etc., but nobody talks about "Curse of Javascript"

I learned Lisp (once) and that opened up path to Clojure, Clojurescript, then Fennel, Janet and Clojure-Dart, libpython-clj, there's Jank that is about to break loose. And something opposite to fragmentation happened to me - all these incompatible runtimes became unified and controllable from the same substrate - I no longer feel like I'm having to switch between languages - the syntax and thinking stays stable. The runtime is just a deployment target.

The curse essay says: "Lisp empowers fragmentation". Actual experience says: "Lisp provides unity across fragmentation that already existed"

Re: A perfectable programming language

#88

Post by d-us-vb »

mghackerlady wrote: post #69
kleiba2 wrote: post #40

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean. Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.

I can't view the site (Org blocks github for reasons) but I suspect this would be a lot like forth if forth weren't so stack focused

Forth is at this point more of a culture than a language. It's a culture about keeping designs simple so that they're understandable. Without this, Forth is only powerful for programmers who can keep a lot in their heads, but lots of Forth programs end up being write-once. Moore's view, as well as most other high-level Forthers preach simplicity above all; a code cleanliness that would make Uncle Bob blush.

Lean and most type theoretic-based languages don't merely preach simplicity, they demand it. A function or type with a handful of terms or constructors might be provably inhabited/total, whereas one with 2 handfuls of terms or constructors might not be in a reasonable amount of time due to the exponential growth of the proof space. Factoring code optimally for provability yields the simplicity that Forth programmers are striving for.

Re: A perfectable programming language

#89

Post by iLemming »

kleiba2 wrote: post #40

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean. Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.

> Homoiconicity anyone?

I'm just leaving this here for anyone interested, seems relevant: https://github.com/replikativ/ansatz

Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4.

Re: A perfectable programming language

#90

Post by ux266478 »

addaon wrote: post #83
ux266478 wrote: post #81

Earlier quoted context omitted.

Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.

Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.

Idris is rather unique in that the development flow involves writing out your program as a trellis with "holes", and you work through your codebase interactively filling those holes. It feels like Haskell with an even more powerful type system and a companion expert system to alleviate the burden that the type-system's power entails. You're still basically always in program-land, mentally.

F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman.

Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc.

You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.

Post reply on HN