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

The seven programming ur-languages (2022)

madhadron.com

Post reply on HN
Print view View original

41–50 of 161 posts

Re: The seven programming ur-languages (2022)

#41

Post by capitalsigma »

tromp wrote: post #37
burakemir wrote: post #18

This article is full of gross mistakes. For example it claims that Caml is "Cambridge ML" which is ridiculously false. Fact check every sentence. Really sad.

Caml was originally an acronym for Categorical Abstract Machine Language [1]. [1] https://en.wikipedia.org/wiki/Caml

Supposedly it was named "caml" because the author was a smoker who enjoyed camel cigarettes, hence the joke that [later implementations](https://en.wikipedia.org/wiki/Caml#History) were named "Caml Light" and "Caml Special Light"

Re: The seven programming ur-languages (2022)

#42

Post by mellosouls »

justincormack wrote: post #11
mellosouls wrote: post #10

(2022) and unfortunately advice to spend significant amounts of time in learning multiple languages is becoming rapidly redundant in the LLM age.

These are tools for thinking with, so not obsolete.

Agree (redundant, not obsolete), but there are better tools for the job in terms of the production value gained in terms time and mental energy spent in mastering them. You can certainly think less as tech becomes more powerful in a domain; I wouldn't advise that either.

Re: The seven programming ur-languages (2022)

#43

Post by andai »

LeCompteSftware wrote: post #31
nextaccountic wrote: post #27

Earlier quoted context omitted.

> Agda, Idris, etc. are functional languages extended with complex types I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language…

This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you…

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.

Re: The seven programming ur-languages (2022)

#44

Post by nextaccountic »

LeCompteSftware wrote: post #31
nextaccountic wrote: post #27

Earlier quoted context omitted.

> Agda, Idris, etc. are functional languages extended with complex types I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language…

This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you…

I mentioned this later

> You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean

What I meant is that the part of Idris that lets people prove theorems is the non-total part

But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages

Re: The seven programming ur-languages (2022)

#45

Post by nextaccountic »

andai wrote: post #43
LeCompteSftware wrote: post #31

Earlier quoted context omitted.

This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you…

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

Yes 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

Re: The seven programming ur-languages (2022)

#46

Post by LeCompteSftware »

Lots of us are having fun identifying our choice for missing family :)

One I might suggest is scripting languages, defined loosely by programming tools which dispatch high-level commands to act on data pipelines: sed, AWK, the sh family, Perl, PowerShell, Python and R as honorary members. In practice I might say SQL belongs here instead of under Prolog, but in theory of course SQL is like Prolog. Bourne shell might be the best representative, even if it's not the oldest.

AWK et al share characteristics from ALGOL and APL, but I feel they are very much their own thing. PowerShell is quite unique among modern languages.

Re: The seven programming ur-languages (2022)

#48

Post by jasperry »

macintux wrote: post #3

Reminds me a bit of Bruce Tate’s approach in 7 languages in 7 weeks, which is where I first encountered Erlang. I think from a historical perspective, describing COBOL and Fortran as part of the ALGOL family is a stretch, but I suppose it’s a good reminder that all history is reductive.

Does anybody know whether Fortran is older or younger than Algol? From Wikipedia, it looks like they were both developed around 1957. Was there any overlap in the design?

Re: The seven programming ur-languages (2022)

#50

Post by otabdeveloper4 »

sennalen wrote: post #47

C++ has Algol roots, but I think the C++ template metaprogramming style is an ur-language of its own. You could draw some parallels with ML maybe, but they came at it from a different direction.

This. Misses the compile-time evaluation boat completely, even though the proverbial "sufficiently smart compiler" is based on the idea.
Post reply on HN