solrize

joined 1 year ago
MODERATOR OF
[–] solrize@lemmy.world 1 points 16 hours ago* (last edited 16 hours ago)

Dependent types only make sense in the context of static typing, i.e. compile time. In a dependently typed language, if you have a term with type {1,2,3,4,5,6,7} and the program typechecks at compile time, you are guaranteed that there is no execution path through which that term takes on a value outside that set. You may need to supply a complicated proof to help the compiler.

In Ada you can define an integer type of range 1..7 and it is no big deal. There is no static guarantee like dependent types would give you. Instead, the runtime throws an exception if an out-of-range number gets sent there. It's simply a matter of the compiler generating extra code to do these checks.

There is a separate Ada-related tool called SPARK that can let you statically guarantee that the value stays in range. The verification method doesn't involve dependent types and you'd use the tool somewhat differently, but the end result is similar.

[–] solrize@lemmy.world 2 points 18 hours ago* (last edited 17 hours ago) (1 children)

Look on Starlink.com. I don't expect it's much worse than your typpical evil ISP or phone caerrier in terms of privacy. Certainly you could route everything through a VPN and that might help a little.

Edit: oh wait, I confused this thread with a different one when I looked at my inbox. Starlink is a high speed service with a roof antenna. For satellite phone stuff, look at https://skylo.tech.

[–] solrize@lemmy.world 9 points 18 hours ago (6 children)

I'd either get an older model for cheap, or get a 9 because of the satellite capability. I wonder if GrapheneOS supports the latter, and for that matter whether it supports the 9 at all yet.

[–] solrize@lemmy.world 2 points 19 hours ago* (last edited 18 hours ago)

I've never owned a home but what people have told me is that you will spend 13 or 14 monthly payments per year, 12 of them on the loan, and the other 1 or 2 on the related expenses. Insurance has gone up a lot around here since then though.

I know you can rent a tiny home plot with water and sewer in the (expensive) SF Bay Area for $800/month including some amenities (deltabay.org) so that is sort of an upper bound. This includes an electric hookup but you have to pay by the KWH for power. You can order a 400 sq foot tiny house (container home) on Amazon for about $20K (https://www.amazon.com/dp/B0D9Q3391S) though that's just for illustration purposes. I don't know enough about them to actually recommend that approach, plus I hate Amazon. So I would try to buy direct if I pursued that.

Mobile internet coverage is pretty good now, unless you're waaay out in the boonies to the point where you have to ask whether there are even roads to get there with. So if you don't use a lot of data, that gets you online fairly inexpensively. The next thing after that is Starlink, which is way less expensive than I thought, $300 for the dish tranceiver plus around $150/month for "unlimited" service.

The deal with well water depends a lot on the location. In the western states there are often legal restrictions. In drier places you have to drill very deep, which is expensive. If there is surface water, it's less bad. In the desert (Joshua tree), a 1000 gallon truck delivery is around $100 (10 cents a gallon) iirc. I looked into this because a friend was interested in building a biodome there. So you are ok for careful usage but typical suburban use with frequent laundry and toilet flushing could get expensive. If you use a well, you might have to process the water to get rid of dissolved metals and solids, some of which can be toxic.

Propane, again, some company delivers a 400 pound tank every few months, which means there has to be a road that can get it there, or you need some other way (ATV) to move it. I guess you can use smaller tanks if that's easier. A friend of mine had this and I think they swapped the tanks around, as opposed to refilling stationary tanks from a truck, but I can ask her. It's possible that I'm confused.

Solar electricity and solar hot water are very doable now. You can buy a pretty good ready-made battery bank from Home Depot or similar, almost as cheaply as you can DIY without serious scrounging. Again I know a guy with around 10KW of solar panels and 10KWH of batteries iirc. He may have spent around $15K on this though he DIY'd. There is a substantial tax credit against solar expenditures here in CA, plus he gets paid when he feeds surplus power back to the utility (net metering), so he is doing pretty well with it. I think that setup is enough to run all normal household stuff most of the time. Maybe you want a backup generator around.

There is a really good old reddit post about solar hot water. I think it is here: https://old.reddit.com/r/diySolar/comments/b5leqm . The person made a huge coil of black PVC tubing exposed to the sun, with the water circulating through a big tank, and this was enough to give him plenty of hot water year-around with a few K$ worth of stuff, plus electricity to run the pumps.

Lately there are developments in ways to extract water directly from atmospheric humidity, even in the desert. I like to say that this is just like the moisture farming I used to do back on Tattooine ;). Web search: "atmospheric water harvesting". Maybe this will become practical soon.

There are a lot of homesteading forums that might be better places to discuss this stuff.

Is there a location you are thinking about? For now, my own interest is sort of academic, but I have been following stuff a little bit.

All told though, I always hear that city and suburban nerds like me often think this lifestyle sounds great, but they get sick of it quickly when they actually attempt it.

[–] solrize@lemmy.world 1 points 20 hours ago (2 children)

In Ada? No dependent types, you just declare how to handle overflow, like declaring int16 vs int32 or similar. Dependent types means something entirely different and they are checked at compile time. SPARK uses something more like Hoare logic. Regular Ada uses runtime checks.

[–] solrize@lemmy.world 1 points 22 hours ago

Nobody intentionally creates vulnerabilities, but more complicated software is more error prone and therefore more likely to be vulnerable. Fast release cycles also get in the way of good testing. The most complicated piece of software on most phones is the web browser, and its complexity is imposed by the web and its advertisements, rather than by what the user wants or needs.

IOS and Android face pretty much the same issues on the OS developer and phone manufacturer sides. Therefore, the IOS and Android worlds could both clean up their acts in about the same way if the incentives were right. That they don't do so might be a bad situation that we have to cope with, but we shouldn't pretend that it is a good situation.

I wonder what apps require IOS 16 in some meaningful way. I know there is a situation with Android apps requiring OS upgrades unnecessarily.

Why do companies like McDonalds want you to run an app anyway, instead of e.g. using a web page? There are a few sites or products where I currently give up the equivalent of a french-fry discount rather than run their stupid app. It's just a minor annoyance so far, but it doesn't make sense to me. Do those apps usuallly keep running the background so they can track you, or what?

[–] solrize@lemmy.world 2 points 23 hours ago (2 children)

Those security vulnerabililties are because of buggy old software, and updating the software in the old devices does as good a job of fixing the vulnerabilities as selling you a new device does. A significant e-waste tax on every new device, accompanied by credits for keeping old devices working, might help with that. Anyway, if it's an app (rather than OS) vulnerability and you can't fix it with an update because the new version of the app requires a new OS, that's mostly likely an app that you don't need to use. I'm getting by ok with F-droid apps instead of Play Store apps, for example.

Best still would be to debug the software before shipping it, so it wouldn't have those vulnerabilities in the first place. There are various forces that get in the way of that, but a significant one is that web development is now driven by delivering more advertising rather than useful information to the user.

[–] solrize@lemmy.world 1 points 23 hours ago* (last edited 23 hours ago)

I wasn't aware of the USB-C adapter with pass through charging, but still, it's extra crap plugged into your phone. Yes I have a Moto G series phone which is Motorola's budget to low-midrange line. It has a headphone jack and it is full size. Flagship phones have a few more features but none seem important.

[–] solrize@lemmy.world 6 points 1 day ago (6 children)

The laptop (Thinkpad X220) that I'm using is much older than the iphone 7 and it runs current Debian just fine. Lots of people are running current LineageOS on similarly old Android phones. Why can't the phone vendors do the same? Planned obsolescence doesn't change by wrapping it with nice marketing words.

I have figured that if I needed to get an iphone for some reason, it would be a 6+, since that is the last version with a headphone jack (similarly for Pixels, it would be a 4A). But I guess that strategy won't work any more.

https://kevinboone.me/headphonejack.html

[–] solrize@lemmy.world 14 points 1 day ago

That's no moon. It's a space station.

[–] solrize@lemmy.world 2 points 1 day ago (4 children)

In Ada, the overflow behaviour is determined by the type signature. You can also sometimes use SPARK to statically guarantee the absence of overflow in a program. In Rust, as I understand it, you can control the overflow behaviour of a particular arithmetic operation by wrapping a function or macro call around it, but that is ugly and too easy to omit.

For ordinary integers, an arithmetic overflow is similar to an OOB array reference and should be trapped, though you might sometimes choose to disable the trap for better performance, similar to how you might disable an array subscript OOB check. Wraparound for ordinary integers is simply incorrect. You might want it for modular arithmetic and that is fine, but in Ada you get that by specifying it in the type declaration. Also in Ada, you can specify the min and max bounds, or the modulus in the case of modular arithmetic. For example, you could have a "day of week as integer" ranging from 1 to 7, that traps on overflow.

GNAT imho made an error of judgment by disabling the overflow check by default, but at least you can turn it back on.

The RISC-V architecture designers made a harder to fix error by making everything wraparound, with no flags or traps to catch unintentional overflow, so you have to generate extra code for every arithmetic op.

[–] solrize@lemmy.world 7 points 2 days ago (7 children)

It's very hard for "Safe C++" to exist when integer overflow is UB. Rust also gets it wrong, though not quite in the same way. Ada gets it right.

 

Blog post by crypto professor Matthew Green, discussing what Telegram does (I wasn't familiar with it) and criticizing its cryptography. He says Telegram by default is not end-to-end encrypted. It does have an end-to-end "secret chat" feature, but it's a nuisance to activate and only works for two-person chats (not groups) where both people are online when the chat starts.

It still isn't clear to me why Telegram's founder was arrested. Green expresses some concern over that but doesn't give any details that weren't in the headlines.

21
Pi Pico 2 Extreme Teardown (electronupdate.blogspot.com)
 

This is a good blog post, with die photos of the new RP2350 chip and a brief description of what they show. There is a link to a 12 minute youtube video that is also very good, that discusses the die shots in more detail and also goes over the rest of the Pico 2 circuit board, including die shots of the QSPI flash chip and the voltage regulator chip.

 

Basically more everything. 2x Cortex M33 cores with floating point, 520KB ram, more PIOs, bunch of secure boot stuff (I have mixed feelings about this), and can boot to a mode with risc-v cores instead of the M33s.

 

I get spammed by them all the time but have so far resisted and stayed with my crappy, slow, and expensive ADSL provider out of principle. But the ADSL provider just raised prices on me AGAIN and it's ridiculous.

What do I do? Is Google Fiber as invasive as other Google stuff? What if I just use it to tunnel a VPN to a non-Google endpoint?

This is sure annoying. It occurs to me that Comcrap might be available here as an alternative, but that must be as evil as Google. At least the ADSL company is reasonable about privacy, as such companies go.

Thanks for any thoughts.

 

It's a pain that search results on lemmy show by default ordered by some useless relevance ranking. I can't think of a single time I didn't want newest first. I couldn't find a preference to request that. It would be great if there was one.

The suggestion on c/support on lemmy.world was to make this kind of request on github, but it seems anti-FOSS to me to require a Microsoft account for a fediverse request, so I'm posting here and hoping for the best.

Thanks for any consideration!

 

Example (spam post containing an amazon affiliate link, post hopefully deleted by now but I assume mods/admins can see it): https://lemmy.world/post/15846936

Also there are tons of links people post legitimately but have tracking parameters, gclid=this, fbclid=that, etc. Those can be cleaned up too.

By editing out these parameters automatically when the link is posted, people's privacy can be protected and the incentive to post affiliate spam can be decreased.

It could be a server config parameter and/or put into the posting UI: "your post contains [link] with flagged parameters, choose between a) post cleaned up version (shown), or b) post link without changes (may go into moderation queue depending on community settings)."

6
submitted 5 months ago* (last edited 5 months ago) by solrize@lemmy.world to c/voyagerapp@lemmy.world
 

Voyager 2.3.1 on Android. I visit a community and select "hide read posts" and those posts disappear a they should. But there is no apparent way to undo this. The pulldown still has "hide read posts" instead of "unhide" them.

 

Sofirn confirmed by email that it is discontinued. No idea about other LT1 series models. A shame. I like the Mini and kind of wanted another one. Oh well.

 
 

New study shows that the default apps collect data even when supposedly disabled, and this is hard to switch off

 

Any idea why? I've been using it for months. I probably had to grant permission when I first installed it, but haven't had to again since then, until just now.

Also, some of the time, when F-droid updates an app, the update just goes through. But other times I get a dialogue asking "do you want to update this app?". It seems random. Any idea?

Phone is a Moto G5 Stylus 2023 and it recently got a security update from Motorola, but I think I've done some F-droid updates since then. However, this may be related.

The other possibility is that something might have happened to F-droid's code signing credentials, e.g. someone messed with them? That thought is basically why I'm asking here.

view more: next ›