nequo

18 ms·

211.
Theorem provers for university math: students' perceptions (2023)(tandfonline.com)
3 points by nequo 2y ago|0 comments
212.
by nequo 2y ago
Condescending towards Emacs users? No. There’s a general theme in Emacs users’ testimonials that you end up doing everything in Emacs. For many that includes web browsing. Hence the joke. It doesn’t include web browsing for me but no condes
213.
by nequo 2y ago
I shouldn’t have to explain a joke[1] but yes: https://www.gnu.org/software/emacs/manual/html_mono/eww.html [1] This phrase is a self-deprecating remark about my own joke making abilities, not a slight a
214.
by nequo 2y ago
Unless you’re an Emacs user. Then it is 100 percent.
215.
Assertion-Evidence talks are comprehended better by audiences(assertion-evidence.com)
1 points by nequo 2y ago|0 comments
216.
by nequo 2y ago
I responded to you in earnest (no AGI needed for the conclusions to hold in this paper) but I’ve realized that you’ve also posted the same link under two other submissions. It is not great practice to plug your own stuff in places where the
217.
Lessons from Formally Verified Deployed Software Systems(arxiv.org)
23 points by nequo 2y ago|0 comments
218.
by nequo 2y ago
My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics. So CompCert seems to me to aim
219.
The CompCert C Compiler(compcert.org)
203 points by nequo 2y ago|225 comments
220.
by nequo 2y ago
> I also use Racket, and I think it is a fine language, but for my use cases it doesn't really come close to the experience with Common Lisp. You mentioned in another comment that you use CL to prototype low-level computations. I as
221.
Some models are useful, but for how long?: When to refit prediction models(arxiv.org)
1 points by nequo 2y ago|0 comments
222.
Why GADTs matter for performance (2015)(blog.janestreet.com)
1 points by nequo 2y ago|0 comments
223.
Loogle: search Lean and Mathlib definitions and theorems(loogle.lean-lang.org)
1 points by nequo 2y ago|0 comments
224.
A type safe Idris2 web framework targeting NodeJS(github.com)
1 points by nequo 2y ago|0 comments
225.
Data Frames for Idris 2(github.com)
2 points by nequo 2y ago|0 comments
226.
by nequo 2y ago
Debugging is a known sore point with OCaml for example. But what is the problem with the Haskell RTS or the OCaml runtime? Why is it not “anywhere as mature” as Python’s or something like Node for JS? Python’s had the GIL while Haskell has
227.
by nequo 2y ago
I think this is right. We routinely check the integrity of the packages and installers that we download using cryptographic hashing. OpenBSD even has a dedicated tool for this purpose.[1] It would make sense to take the same approach with c
228.
by nequo 2y ago
I like the latter much more. I can come up with rationalizations, like my eyes having to travel to the beginning of the long identifiers if I want to tell instance and class apart in the first example but not in the second. But honestly it’
229.
by nequo 2y ago
I_suppose_causality_would_be_difficult_to_establish_here_but_it_is_intriguing_nonetheless._A_little_space_between_words_helps_the_eye_quickly_see_word_boundaries_which_is_helpful_because_in_the_English_language_words_roughly_correspond_to_u
230.
Influencer Cartels(arxiv.org)
4 points by nequo 2y ago|0 comments
231.
by nequo 2y ago
I think I tried and that didn’t fix the Alt+Tab problem for me. The daunting thing about it was that I don’t even know where to begin to track down the cause, and it’s hard to file a bug report because it’s a heisenbug that takes weeks for
232.
by nequo 2y ago
That must be very frustrating. I’m sure you’ve already tried to track down the culprit and it was in vain. All I can say is that the ThinkPad + Sway combination seems solid even with suspend. I’m hoping you’ll find a fix too.
233.
by nequo 2y ago
I’m only talking about window management getting messed up, not power management. My windows always go back to the correct position on the correct monitor with Sway. This was not the case with Gnome on X. Although my experience also matches
234.
by nequo 2y ago
> traditional window managers seem to work better with my brain. My final push came from Gnome (on X11) randomly messing up Alt+Tab so that each time it would start cycling from an arbitrary window rather than the current one, only fixab
235.
Recursive Definitions in Lean(lean-lang.org)
1 points by nequo 2y ago|0 comments
236.
Rust's Unsafe Code Guidelines Reference(rust-lang.github.io)
3 points by nequo 2y ago|0 comments
237.
by nequo 2y ago
> The code on Stack Overflow is already licensed with Creative Commons It is CC-BY-SA so it requires attribution (+ share alike).[1] That is the hard part with code written by LLMs. [1] https://stackoverflow.com/help&#x2F
238.
by nequo 2y ago
It’s not out of touch. It’s a licensing issue. The BSDs were burned by this in the 4.4BSD days.[1] It makes sense that they don’t want to be burned again. [1] https://en.wikipedia.org/wiki/UNIX_System_Laboratories,_Inc.
239.
by nequo 2y ago
Copying functions and not understanding or getting told that it’s garbage?
240.
by nequo 2y ago
What would be the primary benefit of emitting Rust rather than C? Both would be considered safe (assuming Wuffs generates correct code), and Rust could access the C code via FFI. Is there something I’m missing?

More ›