hachyderm.io is one of the many independent Mastodon servers you can use to participate in the fediverse.
Hachyderm is a safe space, LGBTQIA+ and BLM, primarily comprised of tech industry professionals world wide. Note that many non-user account types have restrictions - please see our About page.

Administered by:

Server stats:

9.9K
active users

Oh cool, another Chrome 0-day abusing integer overflow.

Neat.

Great.

Awesome.

Meanwhile, we'll be writing about how we need to have "high impact libraries that help lots of users" and then give examples like CLI Parsing/JSON Parsing before we sit down and go "we should have some standard library types / functions for integers...?".

v.v.v.v. cool prioritization we do here.

Paul Cantrell

@thephd
Swift really got this one right IMO:

+ - * / all trap on overflow.

If you want mod-2^n operations, there are entirely separate operators for that: &+ &- &* &/

There is no implicit conversion between ints of different bit widths, or between ints and floats (in either direction).

Literals implicitly take the contextual type, so there’s no need to explicitly cast, say, `17` to assign it to an Int8 or a UInt64.

Hard to accomplish this consistency anywhere except at the language level.

@inthehands @thephd Better still, actually use the type system. If you write:

i = j * k

then make sure, at compile time, that the type of i can hold the result for any possible values for the types of j and k.

And uint16, etc, aren't types; they're implementations/representations of types. The types we should be using would be something like 0..65536 (or better some number which makes sense for the application rather than an arbitrary number because we happen to be running on a binary computer today).

@edavies @thephd
Once (if) dependent types become usable enough and compile fast enough to work in an industry setting, sure, then we can have that conversation.

We’re a loooong way from there.

@revk Oops, yes, silly of me to have picked a number which had anything to do with binary, let alone get it wrong for many cases.

But a 0..65536 type would be useful in some cases. E.g., to contain the number of bytes in a 64 kB circular buffer.

@inthehands @thephd

@edavies @inthehands @thephd I spent a lot of years using a computer with 16 bit address space, 65535 is stamped in my brain somehow, along with an number of other useful 16 bit decimal numbers.

@edavies @inthehands @thephd That's very difficult; a chain of multiplications gives you a rapidly increasing type size unless you've bounded everything.

@penguin42 Indeed. I doubt it happens that much in practice, though. For most real software you can easily work out what the bounds for various variables are. Automatically proving them is a bit more tricky hence @inthehands 's comment about dependent types, e.g., var i: 0..len(buffer). But it's where I think the next “Rust-like” step forward will come from. Even doing simple cases would take us a long way with most software even if some more difficult cases need a bit more manual intervention to make things really solid.

@thephd

@edavies @inthehands @thephd It looks like Rust does have a (nigjtly) Ranged type:
docs.rs/ranged_integers/latest
I have done a bit of this type of thing in formal proving (using someone elses prover); it's often really hard to pin the range down.

docs.rsranged_integers - RustRanged integers [nightly only]

@penguin42 @edavies @thephd
The concept you’re reaching toward here is “dependent types:” en.wikipedia.org/wiki/Dependen

In short: types can carry logical constraints, e.g. not just “integer” but “integer in a range;” not just “list of T,” but “list of T whose elements are in sorted order.” You can statically verify types like that if and only if you can show the compiler how to •prove• those logical conditions are met — and so…

en.wikipedia.orgDependent type - Wikipedia

@penguin42 @edavies @thephd
…you end up passing around •mathematical proofs• as part of your programming language, which are machine-generated and/or human-written + machine-verified.

It’s a grandiose, confusing dream that is either The Future of Programming™ or a quixotic research exercise, depending on who you ask.

If you’re wondering what it looks like in practice, Lean might be a place to start:
lean-lang.org

lean-lang.orgProgramming Language and Theorem Prover — Lean