momentoftop

5 ms·

1.
by momentoftop 2mo ago
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition? As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contai
2.
by momentoftop 2mo ago
Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) to
3.
by momentoftop 2mo ago
Converting natural language steps to a formal language isn't too challenging. But basically none of those steps will follow directly from the previous steps by any primitive deduction rule of any formal system. From the perspective of
4.
by momentoftop 2mo ago
Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the
5.
by momentoftop 2mo ago
Those manuals were fantastic. I was still coding on our Beeb in the early 90s and I wanted the assembly manual. My dad ordered it from Acorn but it never arrived. Ended up going to the small claims court to get our money back. In the late 9
6.
by momentoftop 3mo ago
I understood that MLton was mostly about performance. It does whole program optimisation and is prepared (or does?) monomorphise just about everything, and applies all of your functors at compile time, so that you've got something more
7.
by momentoftop 3mo ago
Isabelle is still a very active LCF proof assistant, and it's still written in Poly/ML. It's pretty aggressively concurrent under the bonnet, and leverages Poly/ML well for that. There's still HOL4, which predates I
8.
by momentoftop 5mo ago
I also loved: "It looks like they're doing something purposeful and coordinated, something vast --- a timing channel attack on the virtual machine that's running the universe, ..."
9.
by momentoftop 6mo ago
Most of them have simple types and are easy to define in ML or Haskell. I : a -> a I x = x K : a -> b -> a K x y = x W : (a -> a -> b) -> a -> b W f x = f x x C : (a -> b -> c) -> b -&
10.
by momentoftop 6mo ago
Combinators were an attempt to do logic (and computation falls out) without having to mess around with variables and variable substitution, which is annoying and inelegant because you have to worry about syntax issues like variable capture.
11.
by momentoftop 6mo ago
Or better yet, the y combinator is this: W S (Q (S I I)) The whole point is that we don't need no stinking variables.
12.
by momentoftop 7mo ago
> It's extremely rare that you need to (printf "%d %d" foo) I write stuff like `map (printf "%d %d" m) ns` all the time. I daresay I even do the map as a partial application, so double currying.
13.
by momentoftop 7mo ago
Ah, thanks, didn't realise they put the whole manual into the manpage. For other tools (e.g. make), the info manual is complete but the manpage is just a summary.
14.
by momentoftop 7mo ago
Try "info bash" on your system. It's the same manual. In Emacs, when I hit C-h i I get a menu of all my info manuals and I first read the bash one there.
15.
by momentoftop 7mo ago
> The pipe operator works similarly, though it's a combination of fork and dup'ing Any time the shell executes a program it forks, not just for redirections. Redirections will use dup before exec on the child process. Piping wi
16.
by momentoftop 2y ago
Yes, as I said: systems such as Russell's encoded "1", "2" and "+" in such a way that the theorem "1 + 1 = 2" is non-trivial to prove. This doesn't say anything about the difficulty of provi
17.
by momentoftop 2y ago
> Anyone who says AI is useless never had to do the old method of cobbling together git and ffmpeg commands from StackOverflow answers. It's useful for that yes, but I'd rather just live in a world where we didn't have suc
18.
by momentoftop 2y ago
There isn't a serious proof that 1+1=2, because it's near enough axiomatic. In the last 150 years or so, we've been trying to find very general logical systems in which we can encode "1", "2" and "+&q
19.
by momentoftop 2y ago
There's no point as such. They are a natural (non-leaky) generalisation of a recurring pattern in mathematics and software over which you can build some general theory and, in the case of programming languages such as Haskell, a genera
20.
by momentoftop 2y ago
Playing "This thing all things devours" is one of the most profound gaming experiences I have had, and I happened to use Malyon. Why wouldn't I use the best text editor to play an inform game?
21.
by momentoftop 3y ago
"Tuttle? His name's Buttle. There must be some mistake." "Mistake? Ha! We don't make mistakes." Proceeds to drop ceiling plug through ceiling. "That's bloody typical. They've gone back to metric
22.
by momentoftop 3y ago
I love the idea of hanging by a thread, of complete existential and cosmic precarity. To again quote the opening of Call of Cthulhu, science will reveal "our frightful position [in reality]". I like the fact that, for Lovecraft, t
23.
by momentoftop 3y ago
I'm the opposite. One of the things I love about Lovecraft is how oblique the mythology is in his writings. I don't know much about Azathoth, save that he's somehow "Lord of all Things", while being a "Blind Id
24.
by momentoftop 3y ago
The article mentions ST Joshi a few times, who I think deserves credit not just as the foremost scholar of Lovecraft, but possibly for bringing attention to Lovecraft in the 60s and 70s. I thoroughly enjoyed his "Decline of the West&qu
25.
by momentoftop 3y ago
You use them all the time in Haskell and OCaml. Cache locality isn't such an issue. You're not mallocing linked list nodes. You allocate by a pointer bump of the minor heap, and if the GC copies your list into the major heap, it&#
26.
Kids can't use computers (2013)(coding2learn.org)
4 points by momentoftop 3y ago|1 comments
27.
by momentoftop 3y ago
When I started using CL 20 years ago, libraries were stored on cliki and any malicious user could put malware there. Any source you asdf-installed was generally GPG signed and the installer automatically checked signatures against your pers
28.
by momentoftop 3y ago
I have been playing again with CL recently and am doing some trivial web-scraping of an old internet forum. I don't use a REPL directly, but just have a bunch of code snippets in a lisp file that I tell my editor to evaluate (similar t
29.
by momentoftop 3y ago
At various times, I have run a Tor relay node on a spare VPS. I think I stopped in the end because my available bandwidth was pretty below par, and I suspected I wasn't helping the network very much.
30.
by momentoftop 3y ago
Just my understanding of the manpage and TCP forwarding (-L): an SSH connection will be established to the jump host, which then establishes a connection on port 22 to the destination. The local machine now has a forwarded connection to the

More ›