In Rust, `loop {}` is an expression of type `!`, which means that from a type-theoretic perspective it is inhabited. This means that the Curry–Howard correspondence fails for Rust.
> The strongest argument I see for continuing to train much smarter models quickly is the need to build defensive systems against the dangers posed by other AI.
Yikes! I really wonder about the cognitive dissonance necessary to work at OpenAI these days. They’re in an arms race to build a machine god, knowing full well that it could end humanity.
> They’re in an arms race to build a machine god, knowing full well that it could end humanity.
Fantasies built upon extrapolations derived from fever dream delusions. "Could end humanity"? Come on, it's a computer program just like Microsoft Clippy.
It would require an authorized human to load the floppy into the drive and make it go. And there's nothing special about that process being done in code, it could just as well be done by people flipping switches manually.
There's just no plausible way, in the real world, that a computer program running in some datacenter is going to make this happen. Or anything of any dire existential consequence. It's not a real threat.
I think I disagree! You can always manipulate a human. It's true tho that this particular example has a myriad of failsafes, so the actual example I wrote is less than interesting.
Yes, but to make "apocalyptic" scenarios happen your AI would need to manipulate at least millions of people. So far it's not yet clear they can successfully manipulate even one, or even that "manipulate" is a coherent concept, since LLMs pretty clearly have no agency or intrinsic goals. So like... I guess if we start seeing AI systems autonomously throwing elections and starting wars I'd be more concerned? It doesn't look likely anytime soon.
It seems like AI to me as well. “That’s the gap” is a familiar Claude-ism, as are the references to a “pivot” and the use of “touch” to mean “affect”.
To be fair, I’ve reached the point where most random blog posts I read on the internet seem AI written, so it could just be confirmation bias on my part.
KERNEL32.DLL (in spite of the name) provides user-mode system services for the Windows API. The CRT provides the C99 API. There are many entry points to the same thing on Windows; you can do any of `malloc`/`HeapAlloc`/`new`/`VirtualAlloc` to get a void* memory buffer. `malloc` is from the CRT; `HeapAlloc` is from KERNEL32.DLL, and `new` is from the C++ runtime.
Many many different ways to allocate memory. malloc, new, HeapAlloc, LocalAlloc, GlobalAlloc, CoTaskMemAlloc, etc. GlobalAlloc and LocalAlloc are pretty much obsolete. "malloc" sometimes redirects to HeapAlloc with the default process heap, but only sometimes, it depends entirely on which compiler and CRT is used.
It just causes one big headache that a DLL can't simply return a pointer and have the caller use "free", because malloc/free can be incompatible across modules.
This just led to the COM standard, featuring reference-counted objects that don't care what underlying way was used to allocate the memory. For the situations where you do need memory buffers, COM enforces the use of CoTaskMemAlloc/CoTaskMemFree.
The LLM has none, so it relies upon regurgitating what it's ingested, and unsurisingly that includes very little programming Q&A with young children. It has no record of not knowing the answer, and so cannot give this correct response.
Why is subtraction not part of the algebra? It’s certainly familiar to every high school math student. This omission allows the counterexample, so the reveal is a bit of a disappointment IMHO.
Subtraction is not closed over positive integers, which is untidy. The point of Tarski’s conjecture was to propose a minimal number of axioms and operations, AFAICS they define the standard semiring of positive integers (with the natural definition of exponentiation added).
(Edit: positive integers aren’t exactly a semiring because 0 is excluded, although some authors do define a semiring without the requirement of an additive identity element.)
If subtraction is allowed but negative numbers are not, that's known to be undecidable, even without exponentiation. There are several ways to deal with a subtraction with a negative result, but each variant is undecidable.
If we allow negatives but disallow exponentiation, that's decidable. If we allow negatives and partial exponentiation that stays within the integers, that's undecidable again.
If you allow negative integers, you get negative exponents. To accomodate negative exponents, you can expand the domain again, to rational numbers. If you allow rational numbers, then you have to allow rational exponents, which means you can take arbitrary nth roots. Which you could do, but now you're most of the way to the complex numbers (plus roots aren't unique anymore).
I'm not sure, but maybe it is due to that the expression a - b can be replaced as a + (-b)?
Similarly, I think a * b and a / b can be replaced with the same trick, but then I realized it may not work on non-abelian, or where multiplicative inverse is not available...
The subtraction point is interesting but I don't think it makes the result disappointing. The whole point of Tarski's problem is what follows from that very restricted set of elementary identities so finding the exact minimum countermodel under those rules still seems like a pretty satisfying result.
What a beautiful illustration. It makes intuitive the very abstract concepts discussed in the text. It’s fun to zoom in and browse around the structure.
All describable or recognizable complexity is part of the subcountable set of computable subsets of N. Higher infinities thus mostly contain fake elements about which nothing can be said, so they don’t feel any bigger.
"Fake elements," feels right to me. They're allegedly in there but we can't find any of them. It's funny that these elements comprise the majority of the "real" numbers.
It's not about immature people being unable to separate art from artist because it's difficult. The issue is whether it's the right thing to do.
I feel pretty confident that I could describe to you a case (either real or hypothetical) where you would reject an artist based on their personal behavior, rather than their art. You would find it quite difficult in such a case to separate the two.
So the question is where to draw the line, and everyone answers that question differently.
and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".
In the section of (1) also the PDF version is linked:
I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.
It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance
Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!
> I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.
Often the reason is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.
--
If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested
> "HTTP server", "hello world", "todo list app"
in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.
I imagine the quick project showcase would be different for Swift or for Rust.
Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.
Like what kinds of things i can even think of writing with it - an implementation example
> I imagine the quick project showcase would be different for Swift or for Rust.
> Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.
I suggest simply having a look at the table of contents of
This in my opinion gives you a first rough idea for what kind of problems people are using F*.
Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].
This is exactly the reason why I wrote further above:
> Often the reason [why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app"] is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.
> And ideally - what does a simple solution look like in F-star?
RTFM
Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.
> Set me on the path to installing the thing (ideally above the fold)
You are right that someone could go through that effort bat that only really makes sense if they give you some.idea how to use it.
Reading the exchange it seems like you got caught up on the illustrative examples the other person used. If a web server isn't a good example of a simple problem for F* the landing page should have an example of something that is. It shouldn't take going through that many steps to understand the so what.
reply