Conversation

Notices

1. Embed this notice
   ThePhD (thephd@pony.social)'s status on Thursday, 30-Nov-2023 10:47:11 JST ThePhD

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

   Neat.

   Great.

   Awesome.

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Thursday, 30-Nov-2023 10:47:08 JST Paul Cantrell

     in reply to

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

   • Embed this notice
     ThePhD (thephd@pony.social)'s status on Thursday, 30-Nov-2023 10:47:09 JST ThePhD

     in reply to

     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.

     Haelwenn /элвэн/ :triskell: likes this.
     Haelwenn /элвэн/ :triskell: repeated this.
   • Embed this notice
     Ed Davies (edavies@functional.cafe)'s status on Thursday, 30-Nov-2023 23:19:33 JST Ed Davies

     in reply to

     • Paul Cantrell

     @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).

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Thursday, 30-Nov-2023 23:19:33 JST Paul Cantrell

     in reply to

     • Ed Davies

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

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Friday, 01-Dec-2023 01:47:12 JST Paul Cantrell

     in reply to

     • penguin42
     • Ed Davies

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

     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…

   • Embed this notice
     penguin42 (penguin42@mastodon.org.uk)'s status on Friday, 01-Dec-2023 01:47:13 JST penguin42

     in reply to

     • Paul Cantrell
     • Ed Davies

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

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Friday, 01-Dec-2023 01:47:58 JST Paul Cantrell

     in reply to

     • penguin42
     • Ed Davies

     @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:
     https://lean-lang.org

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Friday, 01-Dec-2023 07:53:48 JST Paul Cantrell

     in reply to

     • Petrus Hilarius

     @phf
     It turns out it’s just a fantastically hard problem to solve in a way that’s not a super-annoying partial solution.

   • Embed this notice
     Petrus Hilarius (phf@social.sdf.org)'s status on Friday, 01-Dec-2023 07:53:50 JST Petrus Hilarius

     in reply to

     • Paul Cantrell
     • Ed Davies

     @edavies @inthehands @thephd It's funny that I literally remember writing a post like that in the early 1990s in some German part of USENET that dealt with Oberon. Progress has indeed been ... hampered?

   • Embed this notice
     ThePhD (thephd@pony.social)'s status on Saturday, 02-Dec-2023 07:54:07 JST ThePhD

     in reply to

     We keep calling ourselves software engineers, but engineers elsewhere advance their industry by analyzing failures and building up tools to stop those and make them standard industry practice!

     But we'll just have the same 6 problems, on a regular spin cycle, for like 40 years.