HNHacker News
TopNewBestAskShowJobs

aleph_minus_one

4,928 karma · joined February 14, 2023

submissionscomments
aleph_minus_one··on More German than many Germans
> Culturally, it is hard not feel detached when Germans themselves seem uninterested in cultural aspects that are normally a reason to want to learn a language (literature, films, etc).

I rather disagree:

Many German movies that are produced don't fit my taste (the reasons are a little bit off-topic), and there exist quite a few Germans who think similarly. I could come up with a list of German movies that I like, but this is something that would take a little bit of thinking/effort.

On the other hand, in my experience/observation/bubble many Germans are quite interested in German literature. I could very easily come up with dozens of books of German authors that I like (of course, such a list would be strongly biased by my own taste).

Thus I would claim that (native German) literature is much more deeply ingrained in German culture than (native German) movies, and I am really surprised that you seem to live in a strange bubble where nobody in it seems to be interested in reading belletristic books.

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> Ok, what kinds of problems are they?

> And ideally - what does a simple solution look like in F-star?

RTFM

Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.

> Set me on the path to installing the thing (ideally above the fold)

How to install this thing:

1. Read https://fstar-lang.org/index.html#download

2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases

3. Download F* for an operating system of your choice there.

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> What is code edition?

I think rixed means "code editing" (I guess that rixed is simply not a native (L1) or excellent L2 English speaker).

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> I imagine the quick project showcase would be different for Swift or for Rust.

> Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

I suggest simply having a look at the table of contents of

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

This in my opinion gives you a first rough idea for what kind of problems people are using F*.

Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

This is exactly the reason why I wrote further above:

> Often the reason [why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app"] is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> > F* (pronounced F star)

> No, it isn't.

https://fstar-lang.org/ claims otherwise:

"F* (pronounced F star)".

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> There is no "user case", it's called use case.

Perhaps English is not a native language for zlsa?

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> Examples provide more than syntax. It's the semantics that we care about most.

... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*":

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

> https://fstar-lang.org/tutorial/

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

Often the reason is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

--

If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested

> "HTTP server", "hello world", "todo list app"

in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.

aleph_minus_one··on F*: A general-purpose proof-oriented programming language
> https://fstar-lang.org/tutorial/

FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

> https://fstar-lang.org/index.html#learn (1)

and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

In the section of (1) also the PDF version is linked:

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

aleph_minus_one··on NetBSD 11.0
> MirOS BSD is still around, too.

According to [1],

- the most recent release was from March 16, 2008; 18 years ago

- the most recent preview was from January 17, 2016; 10 years ago

So, despite the fact that the MirOS website [2] has some small News updates from 2026, I would see the evidence on the side that MirBSD is dead, but I would love to be proven wrong on this point.

---

[1] https://en.wikipedia.org/w/index.php?title=MirOS_BSD&oldid=1...

[2] https://www.mirbsd.org/

aleph_minus_one··on NetBSD 11.0
> I often wonder what the current status is of the BSDs (FreeBSD, OpenBSD, NetBSD).

DragonFly BSD ([1], [2]): "Am I a joke to you? :-("

;-)

By the way: If you look for a BSD-based desktop OS, have a look at GhostBSD ([3], [4]) (based on FreeBSD) and/or MidnightBSD ([5], [6]) (forked from FreeBSD). Both are under active development.

---

[1] https://www.dragonflybsd.org/

[2] https://en.wikipedia.org/wiki/DragonFly_BSD

[3] https://www.ghostbsd.org/

[4] https://en.wikipedia.org/wiki/GhostBSD

[5] https://www.midnightbsd.org/

[6] https://en.wikipedia.org/wiki/MidnightBSD

aleph_minus_one··on Physicists Solve a Muon Mystery. Now, Old Results Don't Add Up
> Within the sun, with one exception.

OK, I admit that I never did the actual calculations, but only knew this property of the formulas. :-)

aleph_minus_one··on Physicists Solve a Muon Mystery. Now, Old Results Don't Add Up
Relevant concerning your point:

> What is the most misunderstood historical event?

> The Galileo Affair

> https://tidbits.quora.com/What-is-the-most-misunderstood-his...

aleph_minus_one··on Physicists Solve a Muon Mystery. Now, Old Results Don't Add Up
> Hence I feel heliocentrism is simply an observable fact.

It isn't. You can easily define a coordinate system for the universe in which the earth is the center.

Heliocentrism just makes some approximate computations easier because the sun is so heavy. Thus in heliocentrism, the orbits of the planets are approximately ellipses (near-circles) around the sun, while in a geocentric model, the orbits have more complicated shapes.

Nevertheless (to explicare "approximate" even in the Newtonian gravity model (i.e. not Einsteinian gravity)) be aware that even in the heliocentric coordinate system the earth (and the other planets) don't move along an elliptical (near-circular) orbit around the sun, but both the sun and the planet move around a common center which is near to the sun.

> There is no sane way to put the earth in the center once you do that. [...] Hence I feel heliocentrism is simply an observable fact. It's not a mathematical convenience. It's a fact you can see with a camera. The relativism or perspective argument is irrelevant because as we established you have to be very unreasonable to describe a picture of a huge ass sun that hardly moves with small planets zooming around it as earth centric.

Modern physics really is about that there is no preferred coordinate system: this manifests itself in the fact that conserved quantities can be derived via Noether's theorem from such symmetries in the natural laws. There is just a choice of a coordinate system which in our solar system makes computations easier.

aleph_minus_one··on Ron Gilbert started production on Thimbleweed Park 2
> They need an editor who will go through and identify the puzzles that must be solved through brute force

Barely any adventure game has a puzzle that requires brute-forcing. The problem is rather that sometimes players don't have the same kind of thinking as the developers.

This issue can be aggravated if the player comes from a different culture or is playing a translated version of the game; for a famous example: the "monkey wrench" puzzle only works if the player is used the the US-American English name of the respective tool.

aleph_minus_one··on Ron Gilbert started production on Thimbleweed Park 2
> What these games need is a good old-fashioned Aperture Science Material Emancipation Grill.

For those who are out of the loop:

> https://half-life.fandom.com/wiki/Aperture_Science_Material_...

aleph_minus_one··on Una GPS smart watch – Repairable, USB-C charging, developer-friendly
Well, I guess I am surrounded by a different kind of people ...
aleph_minus_one··on Una GPS smart watch – Repairable, USB-C charging, developer-friendly
> considering that every modern smart phone is both usb-c and waterproof?

I doubt that modern smart phones are waterproof. Who would trust use their smartphone while showering or being in a bathtube (including submerging the smartphone a few centimeters into the water)?

aleph_minus_one··on Una GPS smart watch – Repairable, USB-C charging, developer-friendly
> without uploading it all to surveillance capitalists

I by now often see the term "surveillance capitalists"/"surveillance capitalism" on HN.

While it is a great thing to fight surveillance organizations, don't forget that communist countries had/have (for the latter: People's Republic of China) much worse surveillance in place.

aleph_minus_one··on Why I Left Google DeepMind
Primary source: https://turntrout.com/why-i-left-google-deepmind
aleph_minus_one··on Show HN: Reverse Minesweeper
From the same developer

> https://store.steampowered.com/publisher/divide-the-plunder

I particularly like "Mosaic of the Strange"

> https://store.steampowered.com/app/3444650/Mosaic_of_the_Str...

You will in particular like this game if you are into conspiracy theories. If one switches the difficulty to the hardest one, HN readers might have some fun with this game. :-)

aleph_minus_one··on I wouldn't say Pangram is broken, but I would say that it's brittle
Relevant concerning your point:

> I'm Kenyan. I Don't Write Like ChatGPT. ChatGPT Writes Like Me.

> https://marcusolang.substack.com/p/im-kenyan-i-dont-write-li...

HN discussion:

> https://news.ycombinator.com/item?id=46273466

aleph_minus_one··on Open-weight AI is having its Kubernetes moment
> I’ll be impressed if somebody can make that work considering the vastly larger compute required.

I think you underestimate the computational ressources that the mentioned (and similar-kinded) scientific projects needed. Also consider how much computational ressources people invested into cryptocurrency mining.

No, I think the reasons are different:

- Many companies that train AI model use training data which must not be distributed for copyright reasons (and using it is a legal gray zone)x.

- Also consider that the amount of training data is insane. Scientific projects (and cryptocurrency mining, too) have the property that typically the amount of data (storage requirements) is small (or at least the computation can be partitioned so that each sub-task needs little data), but the required computing ressources are insane.

- AI companies consider a huge part of their training data as their "secret sauce" (they often even paid lots of money to generate it, for example by paying world-renowned experts for writing an answer for some important question).

Thus: Yes, the required computation ressources are huge, but this is a problem for which I consider it to be plausible that it can be solved. The real problems are in my opinion different.

aleph_minus_one··on Open-weight AI is having its Kubernetes moment
> - Unlike OSS where a single volunteer can keep a project going, training costs run into the $billions.

Just some thought: Wouldn't it make sense to build some kind of volunteer computing project to train the next-generation LLM by volunteers, similar to the BOINC [1] projects or Folding@home [2]?

N.B.: BOINC was particularly famous for SETI@home (completed), Einstein@Home, Rosetta@home and PrimeGrid.

I still remember the time when Einstein@Home was in its heyday, and many people who loved putting together fast PCs contributed sometimes even for the reason of showing off in the statistics [3].

---

[1] https://en.wikipedia.org/wiki/Berkeley_Open_Infrastructure_f...

[2] https://en.wikipedia.org/wiki/Folding@home

[3] https://einsteinathome.org/de/community/stats

aleph_minus_one··on If coding has been solved, why does software keep getting worse?
> It doesn't take a 4 year education to learn how to use loops, functions, and basic data structures.

Many employers' understanding of programming is stuck in the era of the 1970s. At that time, this was indeed what programming was about. Since that time, programming has evolved a lot to encompass much more complicated concepts.

aleph_minus_one··on If coding has been solved, why does software keep getting worse?
> If coding has been solved, why does software keep getting worse?

Because the premise that coding has been solved is false. :-)

aleph_minus_one··on Why Software Factories Fail (or: harness engineering is not enough)
> If you’re working on an app or software that has few users, no revenue or minimal revenue, tolerance to bugs is higher and just another Claude prompt away, Software factories are a perfect fit. Most personal software or hobby software or 0-1 yet-to-find-PMF startups belong in this category.

I would rather claim that for my personal/hobby software, I apply a much higher quality standard than for the software that I write at work.

Believe me: I would love to apply the same high (or even higher) standard at work, too.

The problem rather is that it is a very common situation that bosses actively prohibit me from rocking the boat too much. If I make (I think typically good) suggestions, I often get very stern reactions.

At work, elegance is not celebrated - just implement the tasks of users who don't care about quality or elegance.

aleph_minus_one··on Terence Tao's ChatGPT conversation about the Jacobian Conjecture counterexample
> If they made it to college, and can program, they're clearly smart and motivated.

You clearly write from the perspective of the US-American university system.

In Germany, basically everybody can enroll into a computer science program at a university, assuming the person has a Abitur (Allgemeine Hochschulreife) certificate (these terms are difficult to translate into English) from the grammar school [1]. So, "have it made to college" is like "not having been a complete failure in school". [2]

So, making it to the university is no achievement in Germany, and also no sign of motivation either.

> If these courses are so important, they should be taught in a way that students can understand.

These courses are taught in a way that students can understand, but not in a way where you can afford to slack off.

It is basically a consensus in Germany that a university is clearly a wrong place for you if you are incapable of closing knowledge gaps on your own (for example by reading books from the library), and you don't have the self-motivation to sit over the lecture material for hours to finally understand it.

So yes, I would say that among the possible options, weed-out courses in mathematics are in my opinion likely the least bad one.

---

[1] In years where there was an insane demand for places at the university to study computer science such as during the dot-com bubble, there were some restrictions (numerus clausus), but for computer science, this was always the exception to the rule.

[2] There exist good reasons for puns like "Abitur: nichts gerafft und doch geschafft" (Abitur: Didn't get a thing, yet still passed) or "A-bier-tur" (a portmenteau of "Abitur" and "beer", which suggests that even pupils who are more into drinking than learning typically get their Abitur certificate).

aleph_minus_one··on Terence Tao's ChatGPT conversation about the Jacobian Conjecture counterexample
You are talking about (abstract) algebraic structures, and not about rings and algebras (over a ring or field)

> https://en.wikipedia.org/w/index.php?title=Algebra_over_a_fi...

> https://en.wikipedia.org/w/index.php?title=Algebra_over_a_fi...

> https://en.wikipedia.org/w/index.php?title=Associative_algeb...

The latter is what aground asked for in https://news.ycombinator.com/user?id=agrounds

> I’m surprised that rings and algebras would come up in a CS degree. What algorithms topics used those concepts?

aleph_minus_one··on Terence Tao's ChatGPT conversation about the Jacobian Conjecture counterexample
> Having studied CS and maths to post-grad, I think you exaggerate. Although a CS course might use these tools, they didn't in my experience go into explaining or defining them.

I studied computer science (and mathematics) in Germany. I am very certain that this was taught to computer science students, even though (compared to the lectures for math students) the lecturer did not get very deep into these topics.

> most CS students would have been terrified of that.

This is a feature, not a bug. :-)

Seriously: In Germany, the "math for ..." lectures often are intended to be "weed-out lectures" so that students who simply are not qualified for their major get to quit their degree course fast (either by realizing that the degree course is too hard for them, or by (typically) failing math exams so that they get exmatriculated), so that they don't waste many semesters on a degree course which they simply are not suited for.

← PreviousPage 7 of 34Next →