gf000

5 ms·

1.
by gf000 6d ago
Who was looking at a subset of the problem, far from what got published by OpenAI in the end.
2.
by gf000 6d ago
Neural networks barely share anything with actual neurons. A neuron itself is more of a "dumb" computer, so the whole is more like distributed computer system. Also, the cells next to neurons also have essential functionality. Non
3.
by gf000 6d ago
Well, it doesn't have to be novel, does it? Most of the real life problems are probably related to an already solved issue, so intelligent (probabilistic) recall is fruitful, even if it's "unoriginal".
4.
by gf000 6d ago
Care to give some explanation and correction then?
5.
by gf000 7d ago
Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas! That's why I think getting formal verificati
6.
by gf000 8d ago
I agree that physics being simulated is not that easy to handwave away. That's why I mention that brains probably don't "depend" on some quantum-level behavior and a more macro view of physics could be enough. What I mea
7.
by gf000 8d ago
> What does it mean for a "thought" to be computable? Well, given our scientific knowledge it's a molecule-level (only important to disregard quantum physics to make the case easier) physical/chemical process, that we
8.
by gf000 8d ago
Well, I only know how to define computability in terms of Turing machines. For math I don't have a fix definition, but it's surely a bit more specific than that (e.g. I wouldn't consider the computation that prints a 0 at the
9.
by gf000 8d ago
You have infinite steps. Pi is just taking the correct turn an infinite number of times.
10.
by gf000 8d ago
> Most propositions are ugly and irrelevant. Most propositions may be ugly and irrelevant, but how do you know how many are not so and we just can't prove it? Also, what about stuff like Continuum Hypothesis, would you add it or not
11.
by gf000 8d ago
But a 432-state TM is a problem that we would like to "prove" is it not? It's not even a particularly complex one to begin with, my smartwatch has orders of magnitude more state then that and yet here we see that all of our m
12.
by gf000 8d ago
> Math is beyond computation. We are talking about the same thing, but I would actually put this the other way around. Computation and computability is "the final frontier". Math is a "subset" of that. Doesn't ma
13.
by gf000 8d ago
Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression. Also, most of them are made to prove stuff first and foremost and thus trade off a lot
14.
by gf000 8d ago
You should add a strikethrough to your post and post a public apology to the author.
15.
by gf000 8d ago
Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements). I once wrote a pretty disgusting Java-implementation of that concept. And if you didn't use the stdlib, nulls and who knows what
16.
by gf000 8d ago
Not the parent, but that's not the only way to prove stuff, depending on the exact configuration. A bit of a contrived example, but let's say that the user starts at (0,0) and that all the four directions' movement will step
17.
by gf000 8d ago
It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language. Assertions and constraint programming is often runtime only. These languages use depende
18.
by gf000 8d ago
No. It would be weird to stand in line for throwing shit at someone you don't know anything about, and believing that the first guy throwing shit has an actual reason to do so. It turns out everyone in that line is wrong..
19.
by gf000 8d ago
Someone can be a well-known expert in a tiny niche field, and one may be completely unaware of them, or even the whole field. You are splitting hairs for no reason, while standing on the wrong side of this discussion. Feel free to criticize
20.
by gf000 8d ago
Because this shitty blogs' author just called someone "vibe-coding a language with no knowledge about the field" who is literally working in that very field for a decade, long predating LLMs, with numerous high-profile works.
21.
by gf000 8d ago
Probably at the same market where they sell snark. You may want to sell your excess of it, especially that as mentioned there were a popular (as in got to HN frontpage multiple times) version 1 and it's all legit and honest work, getti
22.
by gf000 8d ago
It's a research language, of the more experimental and niche type. No one uses it seriously, and the author since then reverted the nuking of the git history.
23.
by gf000 8d ago
You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project.. > Why would we want the tradeoff where the LLM has to write significantly more
24.
by gf000 8d ago
You mean the SPARK example? Because it's a toy problem and I would definitely not take much away from it. Most proofs are basically write-only and impossible to maintain -- you are better off throwing it away. And I mean human-written
25.
by gf000 8d ago
Hi! I'm just leaving you a comment to counter the influx of negativity coming towards you for no reason. I hope you are doing well and won't take all this too badly -- try to think of it as just free marketing for your project! Ha
26.
by gf000 8d ago
Sure, we can find factors for "verbosity increase" and "difficulty to understand a line" where what you say is also true. I think that java found a decent spot where both factors are low. It's not a particularly ver
27.
by gf000 8d ago
Now define murder!
28.
by gf000 8d ago
Well, I would argue about the first part. Even if they contain "native" text that can be extracted, in most cases their order will be messed up and it is often crucial for correct parsing. So in many cases the visual way is the on
29.
by gf000 8d ago
That doesn't take into account dependencies between tasks, where bottlenecks can happen. In any case, Amdahl's law applies regarding what kind of speedup you can get in such a case.
30.
by gf000 8d ago
Concurrency != parallelism I hope you know and understand the difference. Then strangely enough all my examples will make sense.

More ›