ngruhn

11 ms·

211.
by ngruhn 1y ago
Nice! I didn't know about: :reset-diff-change I've been using git checkout -p But doing this inside Helix is much more convenient.
212.
by ngruhn 1y ago
I was about to write my own tool for this but then I discovered: git diff --color-moved=dimmed-zebra That shows a lot of code that was properly moved/copied in gray (even if it's an insertion). So gray stuff exactly matche
213.
by ngruhn 1y ago
Fair enough. Those website builders have their place. I'm rather thinking of something like NodeRed where you specify control flow. But with boxes and arrows instead of code. Which is also what this Google product seems to do.
214.
by ngruhn 1y ago
Name one successful no-code solution. Not snark. I'm serious. Give me examples. In my experience, these no-code tools either die being too simple or live long enough to be patched into fully fledged visual programming languages. At whi
215.
Check equivalence of any two regex(gruhn.github.io)
2 points by ngruhn 1y ago|0 comments
216.
by ngruhn 1y ago
Would mutual recursion still work with this solution? E.g. function f() { return g() } function g() { return f() }
217.
by ngruhn 1y ago
440+ according to Wikipedia. Only a lower bound I guess. https://en.m.wikipedia.org/wiki/Gaza_Strip_famine EDIT: only due to starvation
218.
by ngruhn 1y ago
I get it. Mental health issues have not been taken seriously in the past to say the least. And we're better off when people can openly talk about them without being ostracized. But you can definitely swing too far in the other directio
219.
by ngruhn 1y ago
Yes, but I don't think it has anything to do with evangelicalism. It's just like Uranus. You can't talk about without it always being a bit unserious.
220.
by ngruhn 1y ago
You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper
221.
by ngruhn 1y ago
fyi: they finally renamed Coq. It's called Rocq now.
222.
by ngruhn 1y ago
With "application" they mean "function application" (aka. calling a function). But I feel you. I'm sure there is a less academic way to explain this stuff. Do you know Lisp or Clojure? Then you already understand la
223.
by ngruhn 1y ago
Very interesting, thanks!
224.
by ngruhn 1y ago
But Turing completeness is also too broad. Otherwise Power point animations and Conways game of life are programming languages.
225.
by ngruhn 1y ago
not sure if that's a good criterion. There are also non Turing complete languages like core SQL or Rocq that definitely feel like programming.
226.
by ngruhn 1y ago
I think everyone who has heard of interactive theorem provers saw that this is going to be a match made in heaven. LLMs reduce implementation effort but pile on massive review effort. Interactive theorem provers reduce review effort but the
227.
by ngruhn 1y ago
Is this easier to analyze than Turing Machine based Busy Beaver?
228.
by ngruhn 1y ago
The mindset that this is righteous. (In theory that "gun owning" part could also be tweaked.)
229.
by ngruhn 1y ago
I mean I agree with the premise but that part is a bit much
230.
by ngruhn 1y ago
And Sudan is having a home grown genocide right now...
231.
by ngruhn 1y ago
I took a course on SMT solvers in uni. It's so cool! They're densely packed with all these diverse and clever algorithms. And there is still this classic engineering aspect: how to wire everything up, make it modular...
232.
by ngruhn 1y ago
True :P On the other hand, laser pointers seem endlessly entertaining.
233.
by ngruhn 1y ago
damn that's very cool stuff
234.
by ngruhn 1y ago
Many use Z3 for type checking like F*, Liquid Haskell, Dafny.
235.
by ngruhn 1y ago
> it's costly to change the shape of something once it's set But in a dynamically typed language you also have that problem. Except there the shape is a hidden assumption and the type checker won't tell you all the places
236.
by ngruhn 1y ago
Why is this flagged? I completely agree. 99% the linter is not enforcing correctness in my experience. It's just enforcing a bunch of subjective aesthetic constraints. Which import order, max number of empty lines between statement, wh
237.
by ngruhn 1y ago
Amazing, that's exactly what I had in mind.
238.
by ngruhn 1y ago
Google can probably infer what I had for breakfast from the way I move the cursor. Can't we have ID-less age verification somehow? Sure, it won't be 100% accurate but keeping out 90% of the kids is a win.
239.
by ngruhn 1y ago
Yeah but the shorter name wins
240.
by ngruhn 1y ago
> I've never heard a decent definition I would say AGI can do every intellectual task a human can do. Maybe the raw cognitive power is already there but scale matters. If it can't work on a task for months on end, it's not

More ›