What would it take to add refinement types to Rust?

Re:What would it take to add refinement types to Rust? by munchler on Tuesday December 24, 2024 @05:22PM (#42505364)

> an integer where the type system would ensure that it is always between 1 and 12

How does Pascal handle overflow/underflow? E.g. Month 10 + Month 11 = Month 21?

[ Parent | on HN ]

Re:What would it take to add refinement types to Rust? by eddsolves on Wednesday December 25, 2024 @02:57AM (#42507584)

I assume modulo?

[ Parent | on HN ]

Re:What would it take to add refinement types to Rust? by loeg on Wednesday December 25, 2024 @10:46AM (#42509319)

Uh, seemingly, yeah. 10+11 = 21. No bounds checking on addition or assignment.

https://onlinegdb.com/3KhhaReLV

[ Parent | on HN ]

Re:What would it take to add refinement types to Rust? by int_19h on Wednesday December 25, 2024 @10:30PM (#42512948)

That is just this one particular implementation of Pascal (unsure which one). The language spec does say that it is an error to assign a value out of range, but as far as what this actually means, it only says that "a complying processor is required to provide documentation concerning its treatment of errors".

[ Parent | on HN ]

Re:What would it take to add refinement types to Rust? by dannymi on Thursday December 26, 2024 @12:11PM (#42516345)

  $ cat a.pp
  {$R+}
  var
    a: 1..12;
    b: 1..12;
    c: 1..12;
  begin
    a := 10;
    b := 11;
    c := a + b;
    Writeln(c)
  end.
  $ fpc a.pp
  Free Pascal Compiler version 3.2.2 [2021/05/19] for x86_64
  Copyright (c) 1993-2021 by Florian Klaempfl and others
  Target OS: Linux for x86-64
  Compiling a.pp
  Linking a
  12 lines compiled, 0.1 sec
  $ ./a
  Runtime error 201 at $00000000004010D8
    $00000000004010D8
    $0000000000422EEC

[ Parent | on HN ]