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

141–150 of 152 posts

Re: A perfectable programming language

#141

Post by nobleach »

anonzzzies wrote: post #111
ux266478 wrote: post #79

Earlier quoted context omitted.

Common Lisp through SBCL fits this for everything but changing GC strategies. I'm not sure why you'd do that, though. SBCL's generational GC is faster in all cases, easy to reason about, and trivial to pause. In many of these other categories, clisp exceeds requirements. The REPL and Doc situation is so good it's honestly worth it for those alone. People put up with `):'(,@ soup for good reason.

I luckily have the freedom to work with SBCL almost fulltime. It is a joy; shame most will never get to experience it (few jobs, parenthophobia etc).

Alright, you and your sibling reply have me wanting to look at it. I wrote Scheme/Racket when I was going through The Little Schemer and SICP. I'll buy a common lisp book. Any recommendations?

Re: A perfectable programming language

#142

Post by codebje »

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?

It's been a little bit since I looked at Idris, so I'll take a closer look now. The QTT behind it struck me as interesting but I didn't play around with it much. Thanks for the tip!

Re: A perfectable programming language

#143

Post by mghackerlady »

blippage wrote: post #132
d-us-vb wrote: post #88

Earlier quoted context omitted.

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…

> Forth is at this point more of a culture than a language. As the saying goes, once you've seen one Forth, then you've seen one Forth. I've mucked around with my own Forths in the past, including one that recognises lexical type, so you could build something like a parser in Forth. I didn't take it that far. Forth is normally conceived as being built from the ground up, but if you're you're going to implement it in…

One of these days I want to make something forth-y as a shell language. I feel like it could work well there

Re: A perfectable programming language

#144

Post by iLemming »

pydry wrote: post #134
ux266478 wrote: post #109

Earlier quoted context omitted.

You're using Lisp software right now! I think this is the most treacherous assumption people tend to make about programming languages, for a few reasons. One of them is that we really don't have any way to measure software that we actually use day to day. Think about the software controlling your local water treatment plant, traffic lights, the software your local power company relies on, the software running the ser…

That's a lot of words to say a lot of FUD. I know people who work in the embedded space working on stuff similar to traffic lights and LISP isnt even on their radar. Rust is. LISP isnt. Every niche language has its fanboys who can end up using it all over the place but when it doesnt spread to non fanboys there is usually a reason to which they are wilfully blind, usually related to its practical value.

> Every niche language

Lisp is not a really a programming language. It is an idea.

Lisp didn't emerge the way most languages do - someone sitting down to design syntax and features for practical software engineering. McCarthy was formalizing a notation for computation itself, building on Church's lambda calculus. The fact that it turned out to be implementable was almost a surprise.

And that origin story matters because it explains why Lisp keeps regenerating. Most languages are artifacts - they're designed, they peak, they fossilize. Lisp is more like a principle that keeps getting re-instantiated: Common Lisp, Scheme, Racket, Clojure, Fennel, Jank. Each one is radically different in philosophy and pragmatics, yet they all share something that isn't really about parentheses - it's about code-as-data, minimal syntax hiding maximal abstraction, and the programmer's ability to reshape the language to match the problem rather than the reverse.

The counterargument, of course, is that at some point the idea has to become concrete to be useful, and once it does, it's subject to all the same engineering tradeoffs as any other language. Rich Hickey for example made very specific, opinionated decisions that are engineering choices, not mathematical inevitabilities. So there's a productive tension between Lisp-as-idea and any particular Lisp-as-language.

> related to its practical value.

Don't be daft, preaching pragmatics to modern Lispers is like trying to explain synaptic connections and their plasticity to neurosurgeons. They already know what's what - tis you who's clueless.

Re: A perfectable programming language

#145

Post by DonaldPShimoda »

noLemming wrote: post #126
DonaldPShimoda wrote: post #117

Earlier quoted context omitted.

Hm. Homoiconicity is not a well-defined term (see, for example, Shriram Krishnamurthi's thoughts [0][1]), but even skimming over that fact, it is a syntactic property, while the quoted line is about semantics . Switching your language to Lisp (or one of its descendents) doesn't gain you anything semantically. [0] Shriram is an original member of the Racket project, so he's been working in the Lisp-like domain for at…

Well, okay Shriram said the term "homoiconicity" is fuzzy, but the underlying thing (the language of data and the language of programs being the same representation) is real and worth taking seriously. Citing him to wave away the whole concept is pretty wild misuse of the citation. They are refining the claim, not negating it. > doesn't gain anything semantically Syntactic properties create semantic affordances. The…

> Citing him to wave away the whole concept is pretty wild misuse of the citation.

Good thing I didn't do that?

> Syntactic properties create semantic affordances.

I don't disagree with this. Benjamin Pierce defines type-checking in the opening pages of Types and Programming Languages as an operation over syntax, for example.

My point was that the parent comment just kind of threw out "homiconicity" when somebody talked about writing properties about a language in that language, and those are entirely separate things. I was addressing a conflation of terms. The property that people generally refer to as "homoiconicity" is useful for things like writing macros, but it does not directly grant you access to any kind of property-checking capabilitiy. I mean, Rust's macro system is far from homoiconic (it's just an AST), but it gives you semantic capabilities. You know?

Re: A perfectable programming language

#146

Post by yuppiemephisto »

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).

https://alok.github.io/assets/lean-position-paper.pdf

i talked about the lisp curse in this old paper. it's rough but explicitly mentions it

Re: A perfectable programming language

#147

Post by yuppiemephisto »

codebje wrote: post #70
harperlee wrote: post #66

Earlier quoted context omitted.

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).

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…

lean IS that language https://github.com/alok/LeanPlot

Re: A perfectable programming language

#148

Post by yuppiemephisto »

shevy-java wrote: post #32

> languages without types tend to grow them, like PHP in 7.4 and Python type annotations Well ... that is a trend that is driven largely by people who love types. Not everyone shares that opinion. See ruby. It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems…

actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exception (and good, but not perfectable lang, one of the inspirations for my remark). typed racket is good but is not culturally central enough. but yeah, i do believe types are [inevitable](https://www.youtube.com/watch?v=0AQdSZqGXz4)

https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe

syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary

Re: A perfectable programming language

#149

Post by yuppiemephisto »

Mathnerd314 wrote: post #102
archargelod wrote: post #65

For anyone as curious as me, here's short description for each language in the list (excluding most common ones): cyclone: safe C dialect preventing memory errors zig: modern systems language with explicit control over memory odin: another modern systems language nim: Python-like syntax, memory safe, compiles to C/C++/JS visual basic: event-driven language for Windows GUI apps actionscript: language for Adobe Flash a…

The author is named Alok, so I would expect alokscript to be a self-authored programming language. But I checked the GitHub profile and I don't see anything.

i was just messing with you guys, but now i'm feeling a bit more motivated

Re: A perfectable programming language

#150

Post by yuppiemephisto »

IshKebab wrote: post #101
unexpectedtrap wrote: post #78

Earlier quoted context omitted.

>It definitely is a bad convention because it's highly surprising. You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?

I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it? The reason they don't do that is because Lean treats proofs as manually generated explicit objects, unlike other languages like Dafny (IIRC) where they are implicit. Requiring explicit proofs for every subtraction was presumably seen as too onerous. Which is fine... BUT they then should have said "so we…

i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you
Post reply on HN