When you run a type checker, it's proving that a program conforms to the type, right? That's why it seems like the incompleteness theorem applies. (Though as I mentioned before, I'm playing a bit loose with the logic.)
1,103 karma · joined August 22, 2011
[ my public key: https://keybase.io/cakoose; my proof: https://keybase.io/cakoose/sigs/gNz7dqjDBzs5anzP30jhCtr5bcogtlGjKLP2yghDN9I ]
I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not?
(I don't have a robust understanding of Godel's incompleteness theorem.)
There appear to be two ways the terms are categorized:
1. "reference counting" and "garbage collection" are two types of automatic memory management/reclamation.
2. "reference counting" and "tracing garbage collection" are two types of garbage collection.
I think mbrodersen is using #1.
(Back in the 90s and 2000s I feel like #1 was much more prevalent. But #2 seems to have gained popularity since then. My theory is that whoever started writing the Wikipedia content for this stuff picked #2.)
This "serverless" part confused me initially, since that term has somehow come to mean "the platform handles routing and scaling up/down your servers".
But this use of the term, "there is no server process", is much more sensible!
That's not what the Pareto principle says, is it? Am I missing something?
> Like followers, standbys are kept up to date asynchronously. This means that it is possible for data to be committed on the primary database but not yet on the standby. In order to minimize data loss we take two very important steps:
> 1. We do not attempt the failover if the standby is more than 10 segments behind. This means the maximum possible loss is 160MB or 10 minutes, whichever is less.
> 2. If any of the 10 segments were successfully archived through continuous protection, but not applied during the two minute confirmation period, we make sure they are applied before bringing the standby out of read-only mode.
> Typically there is little loss to committed data.
AWS RDS and GCP Cloud SQL do synchronous replication, so you are much less likely to lose data in common hardware failure scenarios.
With those options available, a managed DB with async replication is a no-go. I don't understand how so many businesses would be ok with it. (I suspect most people don't even realize that Heroku HA is async.)
Oh yeah -- I'm not at all saying Docker is all bad.
* Like you mentioned, increasing interoperability allows the market be more efficient.
* Docker continued the path that VMs started towards making strong isolation even more efficient and accessible.
* Layers and caching are obviously good for resource consumption.
It's just that the original comment seemed to try shaming the Docker creators about what they've built. All they did was try and make something better. And if they didn't, someone else would have.
> so it’s extremely to just back it up or keep the repo in cloud storage
A single big file seems like it would cause more issues for a generic sync utility. Though I guess I can imagine sync algorithms that work better with one style vs the other.
It's tragedies all the way down :-)
Making a successful tool in a competitive space is hard enough. Asking a creator to somehow factor in environmental impact isn't going to work. A creator that places additional constraints on themselves will more likely lose out to a competitor that doesn't.
This is the kind of thing a carbon tax is perfect for. Cost optimization is infused into how businesses and individuals operate. Tax the things you care about and watch all that machinery get to work!
Right now, people use Docker (and dynamic languages, bloated JS libraries, etc) because burning electricity is the cheapest route. (Sort of... the market's obviously not perfect.) Make electricity expensive enough and we'll get more efficient systems.
And of course taxes aren't the only solution. For example, Google Flights now shows the carbon cost of each flight option, which I think might actually move the needle. But that category of solution might only work in an industry with similar characteristics, e.g. infrequent but large purchases, mature industry that can define measurement standards.
(This bug won't affect the performance comparison, but I was just reminded of how error prone these kinds APIs can be vs the PHP/Python route of having the library function just allocate a new buffer each time.)
https://withinboredom.info/blog/2022/03/16/my-favorite-langu...
> Like, look at this Merge Sort in C# [1] (130 lines) and then look at it in PHP (31 lines) [2]. You can’t beat that kind of productivity, not to mention in PHP, you can even mix data types (like ints and floats) where in the C# version, it’d be much more difficult.
[1] https://github.com/TheAlgorithms/C-Sharp/blob/master/Algorit...
[2] https://www.w3resource.com/php-exercises/searching-and-sorti...
The C# version is the first Google result for "c# merge sort". But a later result is from w3resource.com, which where the PHP code came from. That C# code is only 55 lines and could easily be shorter by replacing loops with standard library calls:
https://www.w3resource.com/csharp-exercises/searching-and-so...
Also, both versions of the code from w3resources.com are trash -- they use an O(N) step to remove an element from the front of the array (array_slice in PHP and List.Remove in C#), which makes them O(N^2 log N), which is even worse than a naive selection sort or bubble sort.
I suspect (hope) that in a few years most billing/payment systems will take care of this for you (either natively or through a seamless partnership) so you just fill out a few forms and forget about it.
It's a common goal. When becoming compliant with sales tax laws, it makes sense to prioritize the states/countries where the business has a physical presence.
https://en.wikipedia.org/wiki/Sales_tax#Enforcement_of_tax_o...
- Logging the exact metrics we wanted to our metrics service. (We wrote a bunch of Lua code to do this.)
- Loading the set of backend services from Zookeeper. (We had a sidecar process that would periodically sync from Zookeeper to a config file, then call `nginx reload`.)
- Routing requests to different datacenters based on where the user's data was homed. (We had Go libraries to do this, and it would have been nice to be able to just call into that. I think we ended up putting this functionality in the sidecar.)
- Changing the way we streamed a response based on an HTTP header from the application. (We ended up writing a C module for this.)
- Changing the backend selection algorithm from "least connections" to "best of 3 random choices". Nginx added support for this in 2018, apparently.
There were ton of things we solved with Lua, which wasn't ideal. Since that's the only Lua in our codebase, everyone who touches it has to make a mental switch to remember all the weird edge cases (as you do with any language), plus 1-based array indexes, plus no static types.
Plus, any Lua or C you write has be contorted to fit Nginx's multi-stage request/response architecture. If you're writing a plugin that is meant to play nice with other plugins, then the contortions may be worth it. But for us, a proxy library would have given us the freedom to write code that was simpler and easier to understand.
The team moved to Envoy after I left: https://dropbox.tech/infrastructure/how-we-migrated-dropbox-...
1. There are already good reverse proxy libraries in C#?
2. There are already good reverse proxy libraries in other languages?
3. There are already good reverse proxy applications?
If it's #1, then yeah, it would be nice if the ReadMe explained why YARP is different. To be fair, they're at least consolidating a bunch of efforts within Microsoft:
> We found a bunch of internal teams at Microsoft who were either building a reverse proxy for their service or had been asking about APIs and tech for building one, so we decided to get them all together to work on a common solution, this project.
If it's #2, then what do C# developers do? Having to build your proxy in another language isn't a deal-breaker, but there are advantages to keeping your project/team/company on a single language.
(And Microsoft does contribute to Envoy [1][2].)
If it's #3, that only works up to a point. My old team used Nginx, which was perfect in the beginning. But over time we needed to customize things in ways that were difficult to do within Nginx's architecture (either in Lua or in C), leading to hackier and hackier solutions. Using a proxy library to build exactly what you need can make things much simpler.
[1] https://blog.envoyproxy.io/general-availability-of-envoy-on-...
[2] https://techcrunch.com/2020/08/05/microsoft-launches-open-se...
Also, it looks like your version also does implicit joins (like EdgeDB), but I'm not sure how they would work in that style.
[1] Or maybe only movies where Zendaya is in the first 5 credited actors; I'm not sure.
Adoption may be the best option for some people in some situations. I can imagine that. But presenting it as an obvious solution to this problem indicates a glaring gap in their understanding of human beings.
I thought the 2014 iCloud hack was because attackers tricked users into revealing their passwords, not because Apple's iCloud service itself was compromised. If that's true, e2e would not have made a difference.
https://en.wikipedia.org/wiki/2014_celebrity_nude_photo_leak
(Of course it's definitely possible for a service itself to be hacked wholesale, in which case e2e would help.)
The answer is Postgres. I have some previous experience with MySQL and there are advantages and disadvantages. The biggest advantage so far is partial indexes.
But since I don't have as much experience with Postgres, there's still the occasional surprise, e.g. index names not being scoped to the table, this collation thing. And from what I've read online, I should probably set up some monitoring for vacuuming issues.
The article about Postgres operational footguns recommends outsourcing those issues by using a managed Postgres service (e.g. AWS RDS or Google Cloud SQL), and that's what I do.
But those preferences may be specific to my situation -- a software developer running an HA web application.
* If you're not a software developer, you might be surprised by the "C" collation, which puts "Z" before "a".
* If you're not running an HA web application, then it's easy to change the collation later -- just dump/restore the DB.
The only supported way to set the database's default collation is at creation time, so I'd need to create a new database, copy the data over, and switch my application over. (There appears to be some Postgres voodoo to change the default collation for an existing database, but that's too risky for me.)
Until I get that done, I need to explicitly specify the collation for all new text fields, e.g.
CREATE TABLE t (
f1 text NOT NULL COLLATE "C"
)
Postgres defaults to the system's collation for UTF-8, which caught me by surprise. Now I'm stuck with a production DB where text prefix queries, which should be a perfect use of a btree, are a full table scan. Probably gonna have to take some maintenance downtime to fix the situation :-\
And more generally about operating Postgres in production: https://blog.nelhage.com/post/some-opinionated-sql-takes/
As for Postgres, I have enormous respect for it and its engineering and capabilities, but, for me, it’s just too damn operationally scary. In my experience it’s much worse than MySQL for operational footguns and performance cliffs, where using it slightly wrong can utterly tank your performance or availability. In addition, because MySQL is, in my experience, more widely deployed, it’s easier to find and hire engineers with experience deploying and operating it. Postgres is a fine choice, especially if you already have expertise using it on your team, but I’ve personally been burned too many times.