Viewing profile — momentoftop

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 th…

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…

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 deduct…

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…

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…

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 func…

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. T…

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, ..."…

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) -> …

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 …

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.

> 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 do…

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.

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.

> 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 …

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 difficult…

> 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 jus…

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 enco…

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 …

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 …

"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 …

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…

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 Th…

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 an…

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…