4 ms·
One feature I wish was more common is the ability to easily range-restrict primitive types, without all the boxing and boilerplate and operator overloading. I
by thrower123 5y ago
One feature I wish was more common is the ability to easily range-restrict primitive types, without all the boxing and boilerplate and operator overloading.
I can write a type that only handles integers 0-10, or floats [0...1], but it is more of a lift than I'd like to do in most cases, inefficient, and so I don't, even though it would be a boon for correctness and avoiding idiot bugs.
- touisteur 5y agoAda 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 agoOr 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 agoOr Idris dependent types, which allows you to prove properties of any value, not just numbers.
- zokier 5y agoAfaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing
- goodpoint 5y agoPlus, Nim supports formal proof natively https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
- touisteur 5y agoHey, 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 agoI 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 agoAda? 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 agoTIL Pascal had those. I'll need to check Turbo Pascal some day. I could have the joys of static bondage typing sooner.
- staticassertion 5y agoRust's const generics eval is quite powerful. It may be able to represent this.
- nynx 5y agoIt probably can't yet on stable, but it will be able to within the next year or so.
- staticassertion 5y agoOh yeah, I guess I should have mentioned I'm talking explicitly about the nightly const feature.