zero_k

9 ms·

61.
by zero_k 2y ago
Correction, Lean4 [1] is sponsored by Amazon, the lead developer, Leonardo de Moura is at AWS now [2]. He was previously at Microsoft Research [3]. Meeting him is a real ride, I only had the chance to talk with him once. [1] https:/&#
62.
by zero_k 2y ago
Yes, we should use LLMs to translate human requirements that are ambiguous and have a lot of hidden assumptions (e.g. that football matches should preferably be at times when people are not working & awake [3]), and use them to create f
63.
by zero_k 2y ago
Wow, nice work [1] ! I used to work on CryptoMiniSat a lot. Nowadays I'm doing model counting and maybe synthesis, if all goes well [2] [1] https://github.com/leanprover/lean4/pulls/bollu [2] https:&#x2
64.
by zero_k 2y ago
Other than cryptography? Like, you see a use-case for it there? Please do educate me! IMO there's nothing there. It's a barren landscape. The desert is more alive.
65.
by zero_k 2y ago
Cadence is a good one. There are also bus/train schedule optimization startups/companies. AWS is also hiring in this field, a lot, but I wouldn't recommend it. Even though many people there are very good, and I respect some o
66.
by zero_k 2y ago
I mean, I wish. I have met these so-called giants of the field when I was at conference (they had a yearly big-brains meeting the same time, same place). I bet they talk about classic stuff because otherwise they wouldn't get funding.
67.
by zero_k 2y ago
By the way, if you truly care about NP-optimization, e.g. MaxSAT algorithms, there's a lot of good work being done, just check out [1]. It's fun, and useful. You could make >$1B just by slightly improving global logistics via s
68.
by zero_k 2y ago
Random k-SAT is useless. I won a number of awards at SAT competitions over the years -- not in random k-SAT, they don't even run that track anymore [1] And I'm pretty damned certain whatever that paper is saying, could be fixed wi
69.
by zero_k 2y ago
You are actively advocating for the death of people. This must be deleted by the OPs ASAP. What is even going on.
70.
by zero_k 2y ago
It's hard to find, sorry. The contact info is here: https://www.hs-augsburg.de/searchwing/de/standorte/ Best to contact: philipp.borgers@searchwing.org
71.
by zero_k 2y ago
Search And Rescue (SAR) is sometimes VERY political. We build long-range RC airplanes to help find boats in distress at sea on the Mediterranean [1]. As you might expect, we could do 10x better, with less resources, if the powers that be wo
72.
by zero_k 2y ago
Honestly, I'm very excited about zig. Lean and mean, and it's written by someone who isn't sitting in an ivory tower, not caring about actual usability. It wasn't designed by a team of PhDs (like, e.g. Haskell), while it
73.
by zero_k 2y ago
If you wanna do it in a flexible way that is very easy to use and essentially the future of ZK, use Powdr [1]. Just write your code in rust nostd and be done with it. It's a compiler, basically. Once you use it, you'll never go ba
74.
by zero_k 2y ago
Exactly. See Sidney Dekker's Field Guide to Understanding Human Error. The posters do (almost) nothing -- other than covering the backside of those who put them up, and doing safety theatre. Looks good, does nothing for safety. The sam
75.
by zero_k 2y ago
Proofs and proof checking is also big in SAT solving (think: MiniSat) and SMT (think: z3, cvc5). It's also coming to model counting (counting the number of solutions). In fact, we did one in Isabelle for an approximate model counter [1
76.
by zero_k 2y ago
100% agree
77.
by zero_k 2y ago
The guarantees would not hold, I'm pretty sure ;) Maybe one of the authors could chip in, but my hunch is that with that you could actually introduce arbitrarily large errors. The beauty of this algorithm really is its simplicity. Of c
78.
by zero_k 2y ago
Not me, the authors -- I'm a fly on the wall compared to them ;) This is some serious work, I just did a fast implementation. Re implementation -- it turns out that there are parts of some standard libraries that this problem pushes to
79.
by zero_k 2y ago
What made me realize is that I saw some snippets of emails he wrote to a colleague. It was... insane. You could see his mind race. He recognized patterns in minutes that would take me days, if not weeks, to recognize. Also, he actually writ
80.
by zero_k 2y ago
I was involved with implementing the DNF volume counting version of this with the authors. You can see my blog post of it here: https://www.msoos.org/2023/09/pepin-our-probabilistic-approx... And the code here: h
81.
by zero_k 2y ago
I am 100% with you. I have infinite admiration for von Neumann's talents. He was the genius of the geniuses. I wish I could have a 10 minute chat with him. He'd blow my mind, I'm sure. I'd love to explain some of the res
82.
by zero_k 3y ago
Just go to an RC field near you, you'll see people flying like that. But don't forget, an RC heli is an accident waiting for a place to happen.
83.
by zero_k 3y ago
Wow, yes, so true! I didn't realize how powerful this kind of fear is. You put it quite well. I'll now have to think about this...
84.
by zero_k 3y ago
Yeah, it's a bulls**t comment. Fools are dime a dozen :(
85.
by zero_k 3y ago
I get you. It took me a looong time to come to terms with the fact that I can buy myself some nice things, even though I was already gifting nice things to others. I still only rarely buy nice stuff for myself, but I am learning. I bought m
86.
by zero_k 3y ago
I read that many (10? 15?) years ago and it changed me. It literally, changed me. That blog post, and its comments (including one by the sister of the author... really difficult stuff) is incredibly hard and important to read.
87.
by zero_k 3y ago
Indeed. If you wanna understand this more in-depth, I suggest the book "Can't Catch a Break: Gender, Jail, Drugs, and the Limits of Personal Responsibility". It does exactly what it says on the lid, an amazing book.
88.
by zero_k 3y ago
Haha null deref is funny. Not surprised they are so bad still. They were terrible back then. Didn't improve over time.
89.
by zero_k 3y ago
This confirms what everyone who ever touched AMD GPGPUs knows -- that the only thing holding back AMD from becoming a 2 Trillion dollar company is their absolutely atrocious software. I remember finding a bug in their OpenCL compiler [1], b
90.
by zero_k 3y ago
The imminent nonsense of fear-mongering and money wasting, mostly. Academic funds spent billions on PQC and academia has been paid to shill nonsense for long enough to convince some of these players to "ah, let's just integrate PQ

More ›