The estimated installed base of macOS machines is 80 million. 400 infections is a tiny proportion of this: 0.0005%, or one in 2,000. That's pretty weird for a virus: how do you manage to create something that is capable of spreading, but so bad at it that it only hits one in 2,000 machines?
I'm not sure if your unit is correct... I am quite sure that you meant £1 per kWh (Kilo Watt Hour) per year.
£1 per Watt for one year. Rough estimate, but it's in the right ballpark. I pay 12p/kWh. That's £0.00012 for 1W for one hour. For one day, it costs £0.00288. For 365 days, it costs £1.0512, so an estimate of £1/Wyear is only 5% off. The unit of kWh per year wouldn't make sense: Watts are a unit of power (energy per unit time). 1kWh is one kW (1000W) for one hour. i.e. my price of £0.12/kWh means that it costs £0.12 to have something that draws 1kW on for one hour (or to have something that draws 100W on for ten hours, and so on). I probably should have written £1/Wyear for consistency with kWh or £1/(W/year), but I assumed that readers could figure it out and was lazy.
A 6 wH router would require 52.56 kW to operate in a year (24/7 and 365 days a year)... So, I don't get the part where you are talking about saving.:-?
What is a 6wH router? Even if you mean 6Wh, that doesn't make sense: how long does it take to consume 1Wh (a unit of energy, not of power)? If you mean a 6W router, then will consume 52.56Wh in one year (not 52.56kW, because that's a unit of power and when you divide by time [i.e. over a year] then you get energy, not power). In contrast, a 60W old PC will consume 525.6kWh. At £0.12/kWh, that works out at £6.3072 to operate the small router or £63.072 to operate the old PC for one year. These numbers are very close to my back-of-an-envelope estimate of £6 vs £60, but more accurately the saving is £56.7648/year, or £113.5296 over two years. If you spend £100 on a low-power embedded router board to replace a 60W old PC that you got for free then you will be £13.5296 better off after two years (assuming electricity prices don't go up and you're on the same-priced tariff as me). After four years, you'll be over £100 better off. The one that I bought lasted 5 years before it was too slow for the network, so that's a saving of £283.824 of electricity. The new version of the same board (three gigE ethernet adaptors and enough CPU power to happily handle line rate on all of them) costs £125, probably around £160 by the time that you've added a case and some flash storage. So over the lifetime of the device (assuming it only lasts five years - I'd actually be quite surprised if GigE is not fast enough in 5 years for most home users), the saving is around £120, more if electricity prices go up. The break-even point is just over two years. As an added bonus, you get a small form-factor device that's silent, so can be hidden in a corner in a room that you actually use, or stored in an under-stairs cupboard without overheating.
Using an old PC for this is likely to be a waste of money and be inconvenient. If you can get £20 for the old PC from someone who actually needs a machine capable of running a GUI, then you're even better off!
Nope. Paintbrush, which shipped with Windows up until 3.11 was a bundled version of ZSoft Paintbrush, with a few features removed and Microsoft branding on top. MS Paint, introduced with Windows 95 (I think, possibly NT 3.x?), was a complete rewrite as a win32 app. The author of TFA doesn't know what he's talking about - it most certainly hasn't been part of Windows since 1985.
You can't do arithmetic: 24 * 365 * 100 = 876000. 24 * 365 * 100 / 1000 = 876. Your 87600 is neither of these numbers and I have no idea how you calculated it. The rough rule of thumb is $1/W/year, with your price estimate it's $1.0512, which is close enough. With 18 cents/kWh, it's $1.5768, but for most of the US $1-2 is the right ballpark. For Germany, it's $3. That doesn't actually detract too much from your main point. You're paying $300/year for power for the 100W machine. A 6W machine that costs $200 will save you over $90 in the first year.
Power here costs about £1/W/year. If you're expecting to keep your router for 2 years, it's worth spending up to £20 to reduce the power consumption by 10W. A typical old desktop will draw around 60W, an embedded router board will draw around 6W. That works out at a saving of £108 over two years, which is about the total cost of the embedded router board (PC-Engines or Soekris). After three years, even if you got the old PC for free, it's still more expensive. I used a PC-Engines WRAP board as my home router for around 5 years before needing to upgrade.
I've seen this from a few ACs, and I have to ask: what are you doing to try to get a job? Are you just sitting at home waiting for recruiters to call (actually, even that seems not to be sufficient to avoid job offers, maybe you've disconnected your phone as well)?
I can't speak for Facebook, as I don't work with them, but most of the people I collaborate with at Google, Microsoft and Apple are over 40, many over 50. And a few of them have been headhunted by these companies very recently (quite a few are former HP or Sun folk). All of these companies are very happy to hire competent older people. They're not; however, happy to keep increasing a salary for someone who has managed to gain age without gaining experience.
So, by using a high-level language, I can get the same sorts of bugs and need the same sorts of work-arounds to avoid them that I used to have to deal with in C, ten years ago before compilers started spotting them automatically and warning me?
The article you link to is about introspection, which is a subset of reflection. With introspection, you can do things like ask what methods an object implements or what fields it has. With reflection, you can do things like replace the implementation of a method at run time. Languages that actually support reflection often integrate it in core ways with the core frameworks. For example, one of the common design patterns in Cocoa is Key-Value Observing, where you register to receive events when a property of an object changes. If you are assigning to instance variables of an object directly, then you need to call some helpers to make this work, but if you use the normal accessors then the framework makes it automatic, by replacing the accessor with an implementation that fires the will-change notification, then calls the original implementation, and then fires the did-change notification. From the page that you linked to, I don't believe that you could implement this in Pascal.
There are a couple of reasons 0-based indexing makes sense. The first only really matters in low-level languages: the indexes represent the offset from the array. The address of array X and index 0 into array X are the same. The second relates to concatenating arrays. The place that you insert into the first array is the length of the array. This idiom crops up sufficiently often that zero-based indexing saves a surprising number of +1 calculations in a program - it's very common for programmers to accidentally clobber the last element in an array in languages that index from 1. Mathematics understands that cardinals and ordinals are different, but programmers often forget...
Semantic whitespace isn't a terrible idea, but like almost everything in Python it's let down by the implementation. Tabs are a variable-width character, spaces are not. Mixing the two in an environment that treats the amount of whitespace as having semantic importance is a recipe for disaster. Python treats a tab as a fixed number of spaces and so the indent that your editor displays is not necessarily the same as what the interpreter picks (I've had to fix a bug in someone else's Python resulting from this[1]). The only sane thing to do is for the interpreter to reject any inputs that mix tabs and spaces at the start of a line as invalid input. I believe that Python now has an option to do that, but it took 20 years to add and it's still an option. This pretty much sums up Python: the obviously sane thing takes 20 years to add to the language and is then optional.
That said, it doesn't bother me nearly as much as a language claiming to support functional programming but not doing tail-call optimisation (1000 recursive calls and your program dies) or else clauses on while loops (another bug in someone else's code that I had to fix was caused by the fact that there are two plausibly sane meanings for this. Python chose the third and the developer assumed they chose one of the others).
[1] My irrational hatred of Python is largely caused by the fact that every time I am given the release version of a Python program I end up finding a bug that I have to fix before I can use it for its intended purpose. No other language manages to be quite this reliable in allowing people to ship completely broken crap that they believe to be working.
Thanks a lot for this overview. It looks like the only active giant is Microsoft, which I interpret as: there's no money to be made there soon.
It's more that Microsoft is the only big tech company that had its reputation hurt badly as a result of poor security. Android security is arguably worse than Windows XP (definitely if you consider how much better it should be given that they had a decade to learn lessons from XP), but Google doesn't yet have a reputation as a vendor of insecure software. Apple invests quite a bit in security, but if you read the list of fixes in the security update from a couple of days ago (including a privilege escalation in the library used for IPC between sandboxed and unsandboxed processes that allows sandbox escape), you can see that they still have a long way to go, yet aren't big malware targets yet. Companies tend to invest in formal verification after some expensive negative PR. Intel did after the FDIV bug, Microsoft after things like Slammer associated 'Windows' and 'insecure' in the minds of their customers.
The thing I don't understand is: how come we still live with internet connected things botnets (CCTVs and such) that can e.g. deal massive DDoS attacks?
Participating in a DDoS doesn't take much and is hard to prevent. If you have a million devices on a 1Mb/s connection, they can easily overwhelm someone on a gigabit connection, even using a sufficiently small amount of their available bandwidth that they won't be spotted at the endpoints. Being able to create a botnet out of these that can launch a DDoS requires a vulnerability and a monoculture. Most software will have at least one exploitable vulnerability, but finding a vulnerability in a thousand different things is prohibitively expensive. If there are a hundred million devices all running the same Linux version or the same network-facing application, then an exploit in that lets you build a botnet.
By the way, DARPA has been funding a lot of research in improving security, including the project that I work on.
It's not about the dead person, it's about the ones still living. Having a photograph of a dead person doesn't make them any less dead, but provides some comfort to those that are left. The same is true of tape recordings of their voice. This is just the next step in that.
100 metres in 24 seconds is not fast. Most people can sprint 100 metres in 13-16 seconds (world record is under 10), almost twice that speed. Speed drops off over distance but most people can run 400m in 60-70 seconds (each 100 metres in 16-17 seconds). If you don't think there's a big difference between these, time your best 100m run and then try to keep the same pace for 1km.
Marathon runners run quite slowly, because they have to keep going for hours. This is how primitive humans caught their prey: not by being faster, but by having a lot more stamina and keeping catching up and forcing the prey to spring until it reached exhaustion. Most humans can run for short periods a lot faster than they can jog a marathon. That said, 15mph is a 4 minute mile, which under a thousand humans have ever done, so if the T. Rex doesn't give up after about 30 seconds then you're probably going to become eaten.
Most things about dinosaurs need to be taken with a very large pinch of salt, because you're often extrapolating entire species from under half a dozen samples of skeletons. The problem is in the translation from the scientific paper to the mainstream news. The first will list all of the caveats and the limits of their model (or be published somewhere crap and ignored by most researchers), the latter will present it as truth.
One of the big problems for our society is that we often teach science as a religion with a set of facts, rather than as a process. When the facts are shown to be incorrect, people lose faith in science, rather than seeing an example of science working precisely as the process is meant to work.
It's swings and roundabouts. With the Samsung, when the vendor stops shipping updates you can probably get them from LineageOS. The Galaxy SII, released in 2011, is still getting updates and runs the latest Android. You lose on first-party updates, but you win on third-party updates. In contrast, the oldest supported iPhone is the iPhone 5, which is now getting only security updates (no new OS) and was released in 2012. When it stops getting security updates, the hardware is effectively useless: the bootloader is locked and so you will never be able to run a non-Apple OS on it.
Tempest attacks are still feasible with modern displays. One of my colleagues does a demo of them at open days. They're also far from the only side channel available. There's a lot of recent work on acoustic side channels. With a modern Android device, any background process that can access the microphones can pick up what you're typing with high accuracy (the iPhone microphones are good enough, but Apple doesn't expose APIs that permit this). Vibration provides similar info and combining the two gives very good accuracy. Anyone who can record what you're typing on an on-screen keyboard can typically see anyway because it shows the characters as they're typed. For physical keyboards, the keys typically make different sounds and it's possible to train models to give quite high accuracy reconstructing from audio. There are also a number of components in a computer that make different ultrasonic sounds that can be used to reconstruct the sound.
Basically, password authentication done anywhere other than a Faraday cage with no windows and no third-party software should not be regarded as protection against an adversary that actually cares.
First, verifying the type system is formal verification, applying the results of a formally verified type system is still just type checking, not verification (except in the loosest possible sense of the word, with about the same level of accuracy as when the press says 'AI' when they mean 'algorithm'). A lot of verification works by reducing the problem to type checking, but in the case of Rust the guarantees afforded by the type system are not correctness according to the specification of your program (the property that you get from verification), they are much weaker (e.g. no data is aliased and mutable at the same time).
Second, unlike that of Pony, the Rust type system is not yet verified and usually this kind of process is iterative, with the type system being found to be unsound during the verification process and fixed. Type systems are assumed to be unsound until they have been verified, type checking against an unsound type system is a long way from verification.
Not always. Pulling in an entire library to run a single function that's 4 lines of code is fairly common, particularly in JavaScript, and is usually more effort than it's worth. But most of the time? Yes.
It can be for cost savings if you have highly bursty workloads. If you need N machines for your peak loads but 0.1N machines most of the time, then something like AWS and only paying for 0.1N machines except during demand spikes is a lot cheaper than hosting N machines yourself. If you have a consistent workload, hosting your own machines is probably noticeably cheaper.
The estimated installed base of macOS machines is 80 million. 400 infections is a tiny proportion of this: 0.0005%, or one in 2,000. That's pretty weird for a virus: how do you manage to create something that is capable of spreading, but so bad at it that it only hits one in 2,000 machines?
I'm not sure if your unit is correct... I am quite sure that you meant £1 per kWh (Kilo Watt Hour) per year.
£1 per Watt for one year. Rough estimate, but it's in the right ballpark. I pay 12p/kWh. That's £0.00012 for 1W for one hour. For one day, it costs £0.00288. For 365 days, it costs £1.0512, so an estimate of £1/Wyear is only 5% off. The unit of kWh per year wouldn't make sense: Watts are a unit of power (energy per unit time). 1kWh is one kW (1000W) for one hour. i.e. my price of £0.12/kWh means that it costs £0.12 to have something that draws 1kW on for one hour (or to have something that draws 100W on for ten hours, and so on). I probably should have written £1/Wyear for consistency with kWh or £1/(W/year), but I assumed that readers could figure it out and was lazy.
A 6 wH router would require 52.56 kW to operate in a year (24/7 and 365 days a year)... So, I don't get the part where you are talking about saving. :-?
What is a 6wH router? Even if you mean 6Wh, that doesn't make sense: how long does it take to consume 1Wh (a unit of energy, not of power)? If you mean a 6W router, then will consume 52.56Wh in one year (not 52.56kW, because that's a unit of power and when you divide by time [i.e. over a year] then you get energy, not power). In contrast, a 60W old PC will consume 525.6kWh. At £0.12/kWh, that works out at £6.3072 to operate the small router or £63.072 to operate the old PC for one year. These numbers are very close to my back-of-an-envelope estimate of £6 vs £60, but more accurately the saving is £56.7648/year, or £113.5296 over two years. If you spend £100 on a low-power embedded router board to replace a 60W old PC that you got for free then you will be £13.5296 better off after two years (assuming electricity prices don't go up and you're on the same-priced tariff as me). After four years, you'll be over £100 better off. The one that I bought lasted 5 years before it was too slow for the network, so that's a saving of £283.824 of electricity. The new version of the same board (three gigE ethernet adaptors and enough CPU power to happily handle line rate on all of them) costs £125, probably around £160 by the time that you've added a case and some flash storage. So over the lifetime of the device (assuming it only lasts five years - I'd actually be quite surprised if GigE is not fast enough in 5 years for most home users), the saving is around £120, more if electricity prices go up. The break-even point is just over two years. As an added bonus, you get a small form-factor device that's silent, so can be hidden in a corner in a room that you actually use, or stored in an under-stairs cupboard without overheating.
Using an old PC for this is likely to be a waste of money and be inconvenient. If you can get £20 for the old PC from someone who actually needs a machine capable of running a GUI, then you're even better off!
Raven, read the post by PhunkySchtuff again. There is no mention of 87600 anywhere.
You might want to try again. He says:
At an optimistic 100W, that's 87600 kWh/year
Looks like it contains the number 87600 to me...
Nope. Paintbrush, which shipped with Windows up until 3.11 was a bundled version of ZSoft Paintbrush, with a few features removed and Microsoft branding on top. MS Paint, introduced with Windows 95 (I think, possibly NT 3.x?), was a complete rewrite as a win32 app. The author of TFA doesn't know what he's talking about - it most certainly hasn't been part of Windows since 1985.
You can't do arithmetic: 24 * 365 * 100 = 876000. 24 * 365 * 100 / 1000 = 876. Your 87600 is neither of these numbers and I have no idea how you calculated it. The rough rule of thumb is $1/W/year, with your price estimate it's $1.0512, which is close enough. With 18 cents/kWh, it's $1.5768, but for most of the US $1-2 is the right ballpark. For Germany, it's $3. That doesn't actually detract too much from your main point. You're paying $300/year for power for the 100W machine. A 6W machine that costs $200 will save you over $90 in the first year.
Power here costs about £1/W/year. If you're expecting to keep your router for 2 years, it's worth spending up to £20 to reduce the power consumption by 10W. A typical old desktop will draw around 60W, an embedded router board will draw around 6W. That works out at a saving of £108 over two years, which is about the total cost of the embedded router board (PC-Engines or Soekris). After three years, even if you got the old PC for free, it's still more expensive. I used a PC-Engines WRAP board as my home router for around 5 years before needing to upgrade.
Why do you think they carry such long poles with hooks on the end?
I've seen this from a few ACs, and I have to ask: what are you doing to try to get a job? Are you just sitting at home waiting for recruiters to call (actually, even that seems not to be sufficient to avoid job offers, maybe you've disconnected your phone as well)?
I can't speak for Facebook, as I don't work with them, but most of the people I collaborate with at Google, Microsoft and Apple are over 40, many over 50. And a few of them have been headhunted by these companies very recently (quite a few are former HP or Sun folk). All of these companies are very happy to hire competent older people. They're not; however, happy to keep increasing a salary for someone who has managed to gain age without gaining experience.
Right now this is attractive because it gives you a potential path to work at big names like Google and facebook.
Which is fairly depressing: come and do CS, you can use your experience to increase the efficiency of advertisements by 0.01%!
Obviously the shepherds can't fly, only the sheep can fly.
So, by using a high-level language, I can get the same sorts of bugs and need the same sorts of work-arounds to avoid them that I used to have to deal with in C, ten years ago before compilers started spotting them automatically and warning me?
The article you link to is about introspection, which is a subset of reflection. With introspection, you can do things like ask what methods an object implements or what fields it has. With reflection, you can do things like replace the implementation of a method at run time. Languages that actually support reflection often integrate it in core ways with the core frameworks. For example, one of the common design patterns in Cocoa is Key-Value Observing, where you register to receive events when a property of an object changes. If you are assigning to instance variables of an object directly, then you need to call some helpers to make this work, but if you use the normal accessors then the framework makes it automatic, by replacing the accessor with an implementation that fires the will-change notification, then calls the original implementation, and then fires the did-change notification. From the page that you linked to, I don't believe that you could implement this in Pascal.
There are a couple of reasons 0-based indexing makes sense. The first only really matters in low-level languages: the indexes represent the offset from the array. The address of array X and index 0 into array X are the same. The second relates to concatenating arrays. The place that you insert into the first array is the length of the array. This idiom crops up sufficiently often that zero-based indexing saves a surprising number of +1 calculations in a program - it's very common for programmers to accidentally clobber the last element in an array in languages that index from 1. Mathematics understands that cardinals and ordinals are different, but programmers often forget...
Semantic whitespace isn't a terrible idea, but like almost everything in Python it's let down by the implementation. Tabs are a variable-width character, spaces are not. Mixing the two in an environment that treats the amount of whitespace as having semantic importance is a recipe for disaster. Python treats a tab as a fixed number of spaces and so the indent that your editor displays is not necessarily the same as what the interpreter picks (I've had to fix a bug in someone else's Python resulting from this[1]). The only sane thing to do is for the interpreter to reject any inputs that mix tabs and spaces at the start of a line as invalid input. I believe that Python now has an option to do that, but it took 20 years to add and it's still an option. This pretty much sums up Python: the obviously sane thing takes 20 years to add to the language and is then optional.
That said, it doesn't bother me nearly as much as a language claiming to support functional programming but not doing tail-call optimisation (1000 recursive calls and your program dies) or else clauses on while loops (another bug in someone else's code that I had to fix was caused by the fact that there are two plausibly sane meanings for this. Python chose the third and the developer assumed they chose one of the others).
[1] My irrational hatred of Python is largely caused by the fact that every time I am given the release version of a Python program I end up finding a bug that I have to fix before I can use it for its intended purpose. No other language manages to be quite this reliable in allowing people to ship completely broken crap that they believe to be working.
Thanks a lot for this overview. It looks like the only active giant is Microsoft, which I interpret as: there's no money to be made there soon.
It's more that Microsoft is the only big tech company that had its reputation hurt badly as a result of poor security. Android security is arguably worse than Windows XP (definitely if you consider how much better it should be given that they had a decade to learn lessons from XP), but Google doesn't yet have a reputation as a vendor of insecure software. Apple invests quite a bit in security, but if you read the list of fixes in the security update from a couple of days ago (including a privilege escalation in the library used for IPC between sandboxed and unsandboxed processes that allows sandbox escape), you can see that they still have a long way to go, yet aren't big malware targets yet. Companies tend to invest in formal verification after some expensive negative PR. Intel did after the FDIV bug, Microsoft after things like Slammer associated 'Windows' and 'insecure' in the minds of their customers.
The thing I don't understand is: how come we still live with internet connected things botnets (CCTVs and such) that can e.g. deal massive DDoS attacks?
Participating in a DDoS doesn't take much and is hard to prevent. If you have a million devices on a 1Mb/s connection, they can easily overwhelm someone on a gigabit connection, even using a sufficiently small amount of their available bandwidth that they won't be spotted at the endpoints. Being able to create a botnet out of these that can launch a DDoS requires a vulnerability and a monoculture. Most software will have at least one exploitable vulnerability, but finding a vulnerability in a thousand different things is prohibitively expensive. If there are a hundred million devices all running the same Linux version or the same network-facing application, then an exploit in that lets you build a botnet.
By the way, DARPA has been funding a lot of research in improving security, including the project that I work on.
It's not about the dead person, it's about the ones still living. Having a photograph of a dead person doesn't make them any less dead, but provides some comfort to those that are left. The same is true of tape recordings of their voice. This is just the next step in that.
100 metres in 24 seconds is not fast. Most people can sprint 100 metres in 13-16 seconds (world record is under 10), almost twice that speed. Speed drops off over distance but most people can run 400m in 60-70 seconds (each 100 metres in 16-17 seconds). If you don't think there's a big difference between these, time your best 100m run and then try to keep the same pace for 1km.
Marathon runners run quite slowly, because they have to keep going for hours. This is how primitive humans caught their prey: not by being faster, but by having a lot more stamina and keeping catching up and forcing the prey to spring until it reached exhaustion. Most humans can run for short periods a lot faster than they can jog a marathon. That said, 15mph is a 4 minute mile, which under a thousand humans have ever done, so if the T. Rex doesn't give up after about 30 seconds then you're probably going to become eaten.
Most things about dinosaurs need to be taken with a very large pinch of salt, because you're often extrapolating entire species from under half a dozen samples of skeletons. The problem is in the translation from the scientific paper to the mainstream news. The first will list all of the caveats and the limits of their model (or be published somewhere crap and ignored by most researchers), the latter will present it as truth.
One of the big problems for our society is that we often teach science as a religion with a set of facts, rather than as a process. When the facts are shown to be incorrect, people lose faith in science, rather than seeing an example of science working precisely as the process is meant to work.
It's swings and roundabouts. With the Samsung, when the vendor stops shipping updates you can probably get them from LineageOS. The Galaxy SII, released in 2011, is still getting updates and runs the latest Android. You lose on first-party updates, but you win on third-party updates. In contrast, the oldest supported iPhone is the iPhone 5, which is now getting only security updates (no new OS) and was released in 2012. When it stops getting security updates, the hardware is effectively useless: the bootloader is locked and so you will never be able to run a non-Apple OS on it.
Tempest attacks are still feasible with modern displays. One of my colleagues does a demo of them at open days. They're also far from the only side channel available. There's a lot of recent work on acoustic side channels. With a modern Android device, any background process that can access the microphones can pick up what you're typing with high accuracy (the iPhone microphones are good enough, but Apple doesn't expose APIs that permit this). Vibration provides similar info and combining the two gives very good accuracy. Anyone who can record what you're typing on an on-screen keyboard can typically see anyway because it shows the characters as they're typed. For physical keyboards, the keys typically make different sounds and it's possible to train models to give quite high accuracy reconstructing from audio. There are also a number of components in a computer that make different ultrasonic sounds that can be used to reconstruct the sound.
Basically, password authentication done anywhere other than a Faraday cage with no windows and no third-party software should not be regarded as protection against an adversary that actually cares.
First, verifying the type system is formal verification, applying the results of a formally verified type system is still just type checking, not verification (except in the loosest possible sense of the word, with about the same level of accuracy as when the press says 'AI' when they mean 'algorithm'). A lot of verification works by reducing the problem to type checking, but in the case of Rust the guarantees afforded by the type system are not correctness according to the specification of your program (the property that you get from verification), they are much weaker (e.g. no data is aliased and mutable at the same time).
Second, unlike that of Pony, the Rust type system is not yet verified and usually this kind of process is iterative, with the type system being found to be unsound during the verification process and fixed. Type systems are assumed to be unsound until they have been verified, type checking against an unsound type system is a long way from verification.
Not always. Pulling in an entire library to run a single function that's 4 lines of code is fairly common, particularly in JavaScript, and is usually more effort than it's worth. But most of the time? Yes.
It can be for cost savings if you have highly bursty workloads. If you need N machines for your peak loads but 0.1N machines most of the time, then something like AWS and only paying for 0.1N machines except during demand spikes is a lot cheaper than hosting N machines yourself. If you have a consistent workload, hosting your own machines is probably noticeably cheaper.