nequo

20 ms·

241.
by nequo 2y ago
Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
242.
by nequo 2y ago
In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?
243.
Wuffs: Wrangling Untrusted File Formats Safely(github.com)
279 points by nequo 2y ago|68 comments
244.
by nequo 2y ago
If this is not a joke, it might actually be a viable idea. It works pretty well for English text, for example: https://arxiv.org/abs/2305.15047
245.
by nequo 2y ago
Setting the temperature to a higher value would emulate this, wouldn't it? Then the model would be more willing to deviate from the most likely next token.
246.
by nequo 2y ago
Haskell implements type classes via dictionary passing that don’t always get optimized away by the compiler so it does have a slight runtime cost: https://okmij.org/ftp/Computation/typeclass.html#dict In Rust, usi
247.
by nequo 2y ago
> Even Rust struggles with this. The Rust language server seems really good. What have you been missing there?
248.
by nequo 2y ago
What kinds of things are you using them for usually? Is it mostly in C/C++?
249.
by nequo 2y ago
I don't quite understand. You don't update any references when thunks are evaluated, GHC's runtime does. The runtime shields you from any mutation, doesn't it? (Unless you explicitly ask it to let you mutate a value in
250.
by nequo 2y ago
It doesn't take more than two minutes to understand what $ and \x -> y do, and if you start writing out those parentheses, you will also realize why $ is part of idiomatic Haskell.
251.
by nequo 2y ago
$ is short for “put everything to the right inside parentheses” and \x -> y defines an anonymous function. Why do you expect to understand the syntax of a language you never studied?
252.
by nequo 2y ago
The reason it looks the way it does is that forM_ is just a function like any other, not a keyword in a dedicated syntactic construct.
253.
by nequo 2y ago
> allowing procedural/local mutation, but making the procedures themselves 'pure' and taking care to control side effects on the program scale? This is what Haskell does by encouraging you to bundle the part of your code t
254.
by nequo 2y ago
Laziness requires immutability to work well, and that means you need to represent mutations such as IO operations in an immutable cover like the IO monad.
255.
by nequo 2y ago
40 years is a really long time. For a lot of us, that covers the remainder of our lives.
256.
Dynamic type systems are not inherently more open (2020)(lexi-lambda.github.io)
2 points by nequo 2y ago|0 comments
257.
by nequo 2y ago
Every male adult had to serve 2 years in the military in the Eastern Bloc. Yet those regimes were pretty stable.
258.
by nequo 2y ago
You are right. As usual, having an opinion on the internet is hard.
259.
by nequo 2y ago
> if a competitor pays more down the line Unless competition gets regulated away, which Altman is advocating for: he supported the creation of a federal agency that can grant licenses to create AI models above a certain threshold of
260.
by nequo 2y ago
What is the bigger fish in your opinion?
261.
Borrow checking, escape analysis, and the generational hypothesis (2018)(steveklabnik.com)
1 points by nequo 2y ago|0 comments
262.
Java's Virtual Machine and CLR (2009)(stackoverflow.com)
1 points by nequo 2y ago|0 comments
263.
by nequo 2y ago
Why do lists provide better memory locality than arrays? The array already stores its elements next to each other in memory. The compacting GC helps arrange the elements of the list close to each other too, right? Then wouldn’t the compac
264.
Rust Design Patterns(rust-unofficial.github.io)
13 points by nequo 2y ago|0 comments
265.
by nequo 2y ago
An alternative is to keep the lab assignment but grade them on a final exam. Then it is in their interest to do the lab assignment by themselves rather than with an LLM.
266.
by nequo 2y ago
> Second, I'm really fond of the full-disk backup I have running. I has saved my ass several times, allowing me to be back in action in less than an hour with minimal data loss, by simply swapping out the disk and restore. Does ZFS
267.
by nequo 2y ago
That’s an Xwayland thing. If your Obsidian has no Wayland support, it will be blurry with any distro. It looks like newer versions use a newer version of Electron that supports Wayland: https://forum.obsidian.md/t/pleas
268.
by nequo 2y ago
There’s that, and on Ubuntu the hardware enablement stack to support newer hardware on LTS: https://ubuntu.com/kernel/lifecycle
269.
by nequo 2y ago
Bricks and glass panels also don’t exist in nature. Only we humans bring them about, just as we do with concrete.
270.
by nequo 2y ago
Firejail gives more control over the boundaries of the sandbox. So deb + firejail seems superior to snaps to me from a security perspective.

More ›