4 ms·
I don't know, for me this doesn't look enough like C (or anything familiar). I would love a language like C# or Python where you could just put in precondition
by captainmuon 5y ago
I don't know, for me this doesn't look enough like C (or anything familiar).
I would love a language like C# or Python where you could just put in preconditions using the expression syntax of the language, and it would try to prove it. If it can't prove it, it might ask for more facts, give a warning, or add a runtime assertion. As far as I know the only language that does this was the experimental Spec#.
I would even go further and have complex preconditions as part of the types, so you could have say a Person with field "age" < 18 is of type Minor. (I know this is tricky. The objects would be immutable, or you'd only be able to specify Person|Minor and only narrow it with an assertion, for example). Nim has something a little bit in this direction with distinct types, and integer range types.
- touisteur 5y agoThat's exactly what Ada2012 and SPARK2014 did. You write your contracts (preconditions, postconditions, assertions, contract-cases, invariants, type predicates) in Ada syntax and you get both runtime assertions and proof depending on which tool you call (compiler or prover). You give more facts when proof fails. You can tag code as 'ghost' and it's only available for proof tools... To be able to be a bit more 'terse' in assertions, they added quantifiers, expression functions, case- and if-expressions. Lots of small improvements to allow contracts, that are finally a boon to write simpler and clearer code. Everything you're asking for here is available in Ada2012 and SPARK2014.
- nextaccountic 5y agoalso what https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using https://docs.rs/contracts/0.6.0/contracts/ https://docs.rs/contracts/0.6.0/contracts/ and it checks whether they are true here is an example using mirai and contracts: https://github.com/facebookexperimental/MIRAI/blob/master/examples/shopping_cart/src/main.rs https://github.com/facebookexperimental/MIRAI/blob/master/ex... (note: the contracts crate can be used for verifying at runtime as well)
- touisteur 5y agoAh yes, the power of rust's macros. I think there is danger in proposing 'assume' without at least trying to prove it and say you're wrong. I think in spark 'assume' is a guide, but it is checked and it is great, because footguns.
- rjbwork 5y agoC# has https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts https://docs.microsoft.com/en-us/dotnet/framework/debug-trac... But honestly it's not that great of a user experience, though it does seem to have been improved at least a little bit since the last time I used it in ~2016 or so.
- lostmsu 5y agoCode Contracts are mostly abandoned AFAIK.
- dash2 5y agoI think Perl 6 aka Raku allows this, you can say something like `Person but $age < 18`.
- lizmat 5y agoI think the you mean: `subset Minor of Person where *.age < 18`
- b2gills 5y agoThe `but` keyword takes an instance and something to mix into it. So you can say something like this: 0 but True --- Since `True` is a `Bool` it automatically creates a role that has a method `Bool` that returns `True`. my $role = role { method Bool { True }} You can do that manually if you want. 0 but role { method Bool { True }} --- It creates a new subclass of Int and mixes in the role. So: 0 but True Is roughly equivalent to: do { my constant but-true = anon role { method Bool { True }} my $class = anon class :: is Int does but-true {} $class.new( 0 ) }