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

101–110 of 152 posts

Re: A perfectable programming language

#101

Post by IshKebab »

unexpectedtrap wrote: post #78
IshKebab wrote: post #74

Earlier quoted context omitted.

> this is definitely not a bad one It definitely is a bad convention because it's highly surprising. That's what makes it a footgun. > that would be a really annoying thing to use Sure. So maybe provide "unchecked" versions for when people don't want to bother. We've known this about interface design for literally decades. The default must be safe and unsurprising. You need to opt into unsafety.

>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're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".

If they had used something like 1 -_ 2 then that would be much less surprising because you'd think "oh right, it's the special saturating subtraction".

Similarly for Uint8.ofNat it should have been Uint8.ofNatWrapping or similar.

This shouldn't be news.

Re: A perfectable programming language

#102

Post by Mathnerd314 »

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.

Re: A perfectable programming language

#103

Post by unexpectedtrap »

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 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 is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.

>Requiring explicit proofs for every subtraction was presumably seen as too onerous.

Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.

>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".

What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.

Re: A perfectable programming language

#104

Post by rootnod3 »

ux266478 wrote: post #79
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,…

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.

Common Lisp Is exactly that. I wish I could use it at work. All my personal stuff nowadays is CL only. There is no other choice.

Re: A perfectable programming language

#105

Post by rootnod3 »

andersmurphy wrote: post #38
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…

> How about lisp? I was wondering why lisp (and forth) were omitted from the initial list of languages named in the post. I guess Scheme is in the list has ok macros.

I get adding Scheme, but omitting CL seems like a big oversight

Re: A perfectable programming language

#106

Post by patrickmay »

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 came here to comment "We already have Lisp."

Re: A perfectable programming language

#107

Post by never_inline »

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,…

What do you like so much about Kotlin type system, and document / testing of elixir?

Re: A perfectable programming language

#108

Post by patrickmay »

vouwfietsman wrote: post #48
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…

> do not acknowledge trade-offs when it comes to type systems Could you elaborate?

Here's a good summary of the limited evidence for the benefits of strong type systems: https://danluu.com/empirical-pl/

Re: A perfectable programming language

#109

Post by ux266478 »

pydry wrote: post #100
iLemming wrote: post #87

Earlier quoted context omitted.

> 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 bac…

>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. It's also the deficit of code we actually use day to day that is actually written in lisp. I file it under the same heading as haskell - a language that clearly has useful ideas , but...

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 servers you connect to, and all the servers those things connect to. All the infrastructure in between and the infrastructure's own infrastructure. Allegro Lisp's customers are shotgun spread in industries like healthcare, finance and manufacturing. They're paying for it, so we can infer they're using it, but can anybody actually name what software is written in it?

If we play six degrees of separation, accounting for the full gamut of every single computer that does something relevant to your life no matter how distant, how much of that software are you actually familiar with? The fact of the matter is that we genuinely have no broad picture. There is no introspective method to find out what software you are relying on in your day to day life, almost all of it is completely opaque and implicit. To ask "what software do I use?" is to ask an unanswerable question. So to then synthesize an answer is to work with an unsound, unsupported, incomplete conclusion, which is exactly how you end up assuming you don't use software written in Lisp, while directly using software written in Lisp (HN)

Of course, even accounting for the epistemic issue, the premise is still flawed. ATS is a language with 'useful ideas, but...', Haskell is an aging pragmatic kitchen sink. Positioning the latter as the former is almost comedic.

Re: A perfectable programming language

#110

Post by IshKebab »

unexpectedtrap wrote: post #103
IshKebab wrote: post #101

Earlier quoted context omitted.

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 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 is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important. >Requiring…

> Lean can deduce proofs implicitly as well.

Sure, but you still have to explicitly ask it to.

> What is a standard subtraction over natural numbers at all?

If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.

Post reply on HN