• 3 Posts
  • 387 Comments
Joined 1 year ago
cake
Cake day: June 20th, 2023

help-circle



  • solrize@lemmy.worldtoProgramming@programming.devSafe C++
    link
    fedilink
    arrow-up
    1
    ·
    edit-2
    2 days ago

    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.


  • solrize@lemmy.worldtoProgramming@programming.devSafe C++
    link
    fedilink
    arrow-up
    1
    ·
    edit-2
    4 days 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.




  • 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.



  • 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.









  • It was ok at the time, and if it isn’t ok now, that means you want to run something that is too bloated for its own good.

    Really though, special hardware for this doesn’t make too much sense. A raspberry pi with two ethernet interfaces would be great, but if you can live with ethernet plus wifi, the current rpi’s will do it. Otherwise there are lots of similar boards that really do have two ethernet.

    I have not really felt much use for self hosted server hardware at home. I use VPS’s for that and it’s less hassle. Maybe it doesn’t count as completely self hosted, but conceptually it’s a miniature colo box.