5 ms·

Or Nim's subrange types. https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types

by _0ffh 5y ago

mixedCase 5y ago
Or Idris dependent types, which allows you to prove properties of any value, not just numbers.
- zokier 5y ago
  Afaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing
goodpoint 5y ago
Plus, Nim supports formal proof natively https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
- touisteur 5y ago
  Hey, great for Nim. Though I hope they're not /too/ tied to z3. Why3 seems to be the standard SOTA tool for proof: it can harness lots of different SMT solvers (each with their strengths and weaknesses) including z3, cvc4, alt-ergo, but also specific solvers (grappa?). It is at the heart of Frama-C and Spark2014. I also think that not having executable contracts by default (and defining whether you want them in your final program or not - see ghost code) is going to be a pain point in the future. I don't know nim enough to see if the syntax for provable properties is different from nim's ordinary syntax but I feel that it can also be a trap, to have your users learn yet another language for proof. I'm hoping for the best here, and I must say, I'm quite happy to see other languages/environment jump in ! Some years ago you had only industrial support for Frama-C, Spark, and some academic success around JML? I don't know Eiffel's Eve enough to say whether I would consider it 'mature'. Nowadays with the work on Rust by Alastair Reid we're getting some new energy in the domain. Great!
  - goodpoint 5y ago
    > I hope they're not /too/ tied to z3 If you mean having a hard dependency on z3 at compile time or something similar - no, it's not. :)
    - touisteur 5y ago
      I was more thinking of having written the whole verifier to fit/please z3. It can be hard/daunting to move to more 'generic' SMT drivers if done late in a project.

Or Nim's subrange types. https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types

by _0ffh 5y ago

Or Nim's subrange types. https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types

mixedCase 5y ago

Or Idris dependent types, which allows you to prove properties of any value, not just numbers.

zokier 5y ago
Afaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing

goodpoint 5y ago

Plus, Nim supports formal proof natively https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html

touisteur 5y ago
Hey, great for Nim. Though I hope they're not /too/ tied to z3. Why3 seems to be the standard SOTA tool for proof: it can harness lots of different SMT solvers (each with their strengths and weaknesses) including z3, cvc4, alt-ergo, but also specific solvers (grappa?). It is at the heart of Frama-C and Spark2014. I also think that not having executable contracts by default (and defining whether you want them in your final program or not - see ghost code) is going to be a pain point in the future. I don't know nim enough to see if the syntax for provable properties is different from nim's ordinary syntax but I feel that it can also be a trap, to have your users learn yet another language for proof. I'm hoping for the best here, and I must say, I'm quite happy to see other languages/environment jump in ! Some years ago you had only industrial support for Frama-C, Spark, and some academic success around JML? I don't know Eiffel's Eve enough to say whether I would consider it 'mature'. Nowadays with the work on Rust by Alastair Reid we're getting some new energy in the domain. Great!
- goodpoint 5y ago
  > I hope they're not /too/ tied to z3 If you mean having a hard dependency on z3 at compile time or something similar - no, it's not. :)
  - touisteur 5y ago
    I was more thinking of having written the whole verifier to fit/please z3. It can be hard/daunting to move to more 'generic' SMT drivers if done late in a project.