5 ms·

Ada is for you then : https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers https://learn.adacore.com/courses/intro-to-a

Ada is for you then : https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers https://learn.adacore.com/courses/intro-to-ada/chapters/stro...

_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.
mpweiher 5y ago
Ada? Newfangled nonsense. :-)) Pascal! http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/ref_data.doc.html#1143 http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/re...
- touisteur 5y ago
  TIL Pascal had those. I'll need to check Turbo Pascal some day. I could have the joys of static bondage typing sooner.

Ada is for you then : https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers https://learn.adacore.com/courses/intro-to-ada/chapters/stro...

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

mpweiher 5y ago

Ada? Newfangled nonsense. :-)) Pascal! http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/ref_data.doc.html#1143 http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/re...

touisteur 5y ago
TIL Pascal had those. I'll need to check Turbo Pascal some day. I could have the joys of static bondage typing sooner.