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.

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.

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.

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?

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.

https://www.freedombox.org/ ?

About learning more Python? Code up something interesting, or join an existing project and contribute.

About starting freelancing without a track record? Right now it’s difficult, though maybe that’s cyclical. But basically look on Craigslist and so on for help wanted. Stay away from bottom feeders like Fiverr. There is a monthly “who is hiring” post on Hacker News and a similar post for freelancers (mostly work seekers) but the entry barrier there can be sort of high.

See: https://news.ycombinator.com/submitted?id=whoishiring

primarily a gamedev, so no functional programming languages like Rust or Haskell.

Talk to Tim Sweeney.

The Next Mainstream Programming Language: A Game Developer’s Perspective (pdf).

Note that C++ is getting modules, that might speed up compilation, though it’s still C++ afterwards. The cool kids in systems programming are using Rust now. I have no idea if game devs are using it. Anyway, on games projects or anything else, you have to use what the other people on your team are using, which these days is still mostly C++ afaict.

Another sign Python is hosed by abandoning “batteries included”.

If whatever they are doing has been working for stuff written in languages other than Rust, we have to ask what makes Rust special. Rust is a low level language, so its dependencies if anything should be simpler than most, with just a minimal shim between its runtime and the C world. Why does any production software have a version <= X constraint in any of its dependencies anyway? I can understand version >= X, but the other way implies that the API’s are unstable and you’re going to get tons of copies stuff around. I remember seeing that in Ruby at a time when Python was relatively free of it, but now Python has it too. Microsoft at least understood in the 1990s that you can’t go around breaking stuff like that.

No it’s not all C99. I’m using Calibre (written in Python), Pandoc (written in Haskell), GCC (written in C, C++, and Ada), and who knows what else. All of these are complex applications with many dependencies. Eclipse (written in Java) is also in Debian though I don’t use it. Bcachefs though is apparently just special.

Joe Armstrong (inventor of Erlang) said of OOP, “you wanted a banana but what you got was a gorilla holding the banana, and the entire jungle”. Rust begins to sound like that too. It might not be inherent in the language, but it looks like the way the community thinks.

I also still don’t understand why the Bcachefs userspace stuff is written in Rust. I can understand about the kernel part, but the concept of a low level language is manual resource management that a HLL handles for you automatically. Writing the userspace in a LLL seems like more pain for unclear gain. Are there intense performance or memory constraints or what?

Actually I see now that kernel part of Bcachefs is also considered unstable, so maybe the whole thing is not yet ready for production.

Talks about different developer styles, slightly interesting and not too long winded I guess, but not much about the actual situation.

I think this is still not such a great look for Rust. I had expected interfacing Rust to C to present fewer problems than it seems to. I had hoped the Rust compiler could produce object code with almost no runtime dependencies, the way C compilers can. So integrating Rust code into the kernel should be fairly painless from the C side, if things were as one would hope.

It does sound to me in the earlier post that there was some toxicity going on. Maybe it had something to do with the context being a DRM driver.

I looked at a few Rust tutorials but they seemed to take forever to get to any interesting parts. I will keep looking.

Oh man, that isn’t a good luck for Rust. What do those tools do and how much code is there anyway? If they are userspace tools, what is the benefit of writing them in Rust?

Lol, first Tim Peters and now Guido.

Edit: oh LOL2, now I see Guido’s comment at the top of this thread, and in case it went past anyone, it was a reference to Tim Peters.

Very very different.