C, C-like, or Rust
As always, Ada gets no respect.
C, C-like, or Rust
As always, Ada gets no respect.
I’ll look at the wiki article again but I can pretty much promise that Ada doesn’t have dependent types. They are very much a bleeding edge language feature (Haskell will get them soon, so I will try using them then) and Ada is quite an old fashioned language, derived from Pascal. SPARK is basically an extra-safe subset of Ada with various features disabled, that is also designed to work with some verification tools to prove properties of programs. My understanding is that the proof methods don’t involve dependent types, but maybe in some sense they do.
Dependent types require the type system to literally be Turing-complete, so you can have a type like “prime number” and prove number-theoretic properties of functions that operate on them. Apparently that is unintentionally possible to do with C++ template metaprogramming, so C++ is listed in the article, but actually trying to use C++ that way is totally insane and impractical.
I remember looking at the wiki article on dependent types a few years ago and finding it pretty bad. I’ve been wanting to read “The Little Typer” (thelittletyper.com) which is supposed to be a good intro. I’ve also played with Agda a little bit, but not used it for real.
My mom has quite severe hearing loss but is not totally deaf. She uses TV captioning and generally can’t tell whether the TV sound is on or off. I generally want it to be off because it is annoying, so when she leaves it on by accident, I just shut it off and she doesn’t notice or anyway doesn’t care.
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.
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.
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.
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.
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.
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.
They need “This show depicts stupidity” but they will never have it.
I think if your photos are on any kind of public website, AI idiots will scrape them regardless of the provider. So at minimum you have to password protect them. That said, I’d feel ok using this:
https://www.hetzner.com/storage/storage-share/
It basically runs NextCloud. You’d configure it so that only logged-in users can view the pictures, and give accounts to your friends and family. I don’t think Hetzner is likely to train AI with it, though you could check through their privacy policy. Part of the issue with eg. Google Drive is that everyone wants stuff for free, so Google recovers some of its costs by advertising, AI training, etc. Hetzner charges enough to actually make a profit, while still being IMHO affordable at the level we’re discussing. That means they don’t have to do crap with advertising etc. I have 5TB in their Storage Box product and am happy with it.
If you want to be more hardcore, you could set up a dedicated server with an encrypted HDD, but now you have to deal with the hassles of self hosting, including backups. It still wouldn’t be end to end encryption, which would require your users to run some kind of special client, or maybe use some awful javascript client.
It would help if you gave some numbers. How much data, within a factor of 1000 say? A few megabytes? A few gigabytes? A few terabytes? A few petabytes? The approach you need will change depending on the level. What is your budget?
What bothers you about cloud storage? Are any of the photos edgy?
Anyway it sounds to me like you would be fine with a decent web hosting plan and a basic photo gallery app.
You’re broadcasting to family who will likely be using gmail, so what difference does it make? Google will get all the emails either way. Anyway, logical argumentation is completely useless in a personal situation like that.
If you want the address to be stable in the long term, you should probably use your own domain name instead of gmail or proton, if you’re not already doing that. After that, it’s possible to switch the hosting without changing the email address.
Never heard of U-prove but for what you are asking, is FIDO2 similar?
This seems terrible. You can get a nice laptop for a lot less, including some that you can configure as a tablet, e.g. Lenovo Yoga.
I wouldn’t count on google drive doing anything in particular after expiration, unless that is expressly part of the product description. Just because you can observe it happening now doesn’t mean you can expect it to keep happening. For that matter, Google cancels products all the time. So I wouldn’t even rely on the paid plan not being withdrawn at some inconvenient moment. If you really want to use it, then best strategy is probably use it as long as it lasts, but have some plan B in mind if it goes away.
Oneprovider.com shows lots of offers in Istanbul, though servers are expensive there compared to a place like Hetzner:
https://oneprovider.com/search?&cities[]=62&price=0&price_max=9999999999999999&price_any=0
1.1 USD/mo for 2TB is basically a giveaway or free plan, i.e. you’re the product not the customer. So I’d be suspicious. How much storage are you looking for? Hetzner unfortunately jumps from 3.2 euro/1TB to 11 euro/5TB. So 2TB is kind of a bad spot on that scale. But if google drive is working for you and your stuff is encrypted, why not keep it?
Tbh you get jerked around less with paid plans. I’m happy with Hetzner Storage Box. I have 5TB there for 10 euro/month. I’d never use Google Drive. borgbase.com has a 10GB “free forever” plan and I could see parking some stuff there, but 10GB is pretty small and IDK the conditions. Why not use a VPS provider with better storage options?
OOP was a 1990s thing that is still around but don’t worry about it too much at first.
The classic intro book is Structure and Interpretation of Computer Programs aka SICP. You can find it online with a web search. It will give you a good grounding in fundamentals. Then you can figure out what to pursue next.