Readit News1. Complete, Decidable, Well founded are all distinct things.
2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that. https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...
6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
I don't have a problem with compile time code execution potentially not terminating, since it's clear to the programmer why that may happen. However, conventional type checking/inference is more like solving a system of constraints, and the programmer should understand what the constraints mean, but not need to know how the constraint solver (type checker) operates. If it's undecidable, that means there is a program that a programmer knows should type check, but the implementation won't be happy with; ruining the programmer's blissful ignorance of the internals.
https://langdev.stackexchange.com/a/2072
My interpretation
Decidability is of academic interest, and might be a hint if something is feasible.
But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack
And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime
What matters is being able to reject all incorrect programs, and accept most human written valid programs
> [ all non-trivial semantic properties of programs are undecidable ]
https://en.wikipedia.org/wiki/Rice's_theorem
Found here:
From Sumatra to Panama, from Babylon to Valhalla
There are decidable type systems for Turing complete languages (many try to have this property), and there are languages in which all well typed programs terminate for which type checking is undecidable (System F without all type annotations).
Deleted Comment
Though I guess writing like this doesn't pay off in the modern world. Most readers don't consistently pay attention when reading, and to be honest, I don't either.
I agree with you that Quanta doesn't always "allow specialists to understand exactly what's being claimed", which is a problem; but linking to the research papers greatly mitigates that sin.
[1] https://www.quantamagazine.org/the-largest-sofa-you-can-move...
And here's how they clearly explain the proof strategy.
> First, he showed that for any sofa in his space, the output of Q would be at least as big as the sofa’s area. It essentially measured the area of a shape that contained the sofa. That meant that if Baek could find the maximum value of Q, it would give him a good upper bound on the area of the optimal sofa.
> This alone wasn’t enough to resolve the moving sofa problem. But Baek also defined Q so that for Gerver’s sofa, the function didn’t just give an upper bound. Its output was exactly equal to the sofa’s area. Baek therefore just had to prove that Q hit its maximum value when its input was Gerver’s sofa. That would mean that Gerver’s sofa had the biggest area of all the potential sofas, making it the solution to the moving sofa problem.
Since you've asked about bugs, I tried pushing the limits and found the following:
A1: 100 B1: =100-A1
A2: =A1*(100-A1)
A3: =A1*B1
However, setting A3 to exactly 100 doesn't work, even though setting it to 101 or 99 (or even 100.000001) does work.
Another limit:
A1: 100 B1: 100
A2: =A1+B1
A3: =A1*B1
A4: =abs(A2-100) + abs(A3-100)
In case you can't tell from that last example, I think being able to fix the intended values of multiple outputs simultaneously would be interesting. If you were to give more details about the solver's internals, I'd be keen to hear them.
An arbitrarily-perfect simulation of a burning candle will never, ever melt wax.
An LLM is always a description. An LLM operating on a computer is identical to a description of it operating on paper (if much faster).
Thanks for stating your views clearly. I have some questions to try and understand them better:
Would you say you're sure that you aren't in a simulation while acknowledging that a simulated version of you would say the same?
What do you think happens to someone whose neurons get replaced by small computers one by one (if you're happy to assume for the sake of argument that such a thing is possible without changing the person's behavior)?
(-1)ˣ = cos(πx) + i sin(πx) (-1)ˣ = cos(πx) - i sin(πx)
I didn't quite get if Automatic TLS (https://developers.cloudflare.com/ssl/origin-configuration/s...) could use plain transfers.
So:
* Is it insecure by default or you have to be intentionally insecure?
* Why would anyone pick the flexible/potentially-insecure option?
Because having a connection that's encrypted between a user and Cloudflare, then unencrypted between Cloudflare and your server is often better than unencrypted all the way. Sketchy ISPs could insert/replace ads, and anyone hosting a free wifi hotspot could learn things your users wouldn't want them to know (e.g. their address if they order a delivery).
Setting up TLS properly on your server is harder than using Cloudflare (disclaimer: I have not used Cloudflare, though I have sorted out a certificate for an https server).
The problem is that users can't tell if their connection is encrypted all the way to your server. Visiting an https url might lead someone to assume that no-one can eavesdrop on their connection by tapping a cross-ocean cable (TLS can deliver this property). Cloudflare breaks that assumption.
Cloudflare's marketing on this is deceptive: https://www.cloudflare.com/application-services/products/ssl... says "TLS ensures data passing between users and servers is encrypted". This is true, but the servers it's talking about are Cloudflare's, not the website owner's.
Going through to "compare plans", the description of "Universal SSL Certificate" says "If you do not currently use SSL, Cloudflare can provide you with SSL capabilities — no configuration required." This could mislead users and server operators into thinking that they are more secure than they actually are. You cannot get the full benefits of TLS without a private key on your web server.
Despite this, I would guess that Cloudflare's "encryption remover" improves security compared to a world where Cloudflare did not offer this. I might feel differently about this if I knew more about people who interact with traffic between Cloudflare's servers and the servers of Cloudflare's customers.