verus-lang verus Language Design · Discussions

Sort by: Latest activity

Language design Discussions

You must be logged in to vote

Supporting dyn soundly

Chris-Hawblitzel started Mar 25, 2024 in Language design

9
You must be logged in to vote

Consider enforcing termination checking

utaal started Aug 10, 2022 in Language design

3
You must be logged in to vote

Next-generation of Tracked/Ghost code

tjhance started Oct 9, 2024 in Language design

14
You must be logged in to vote

Improve error messages

utaal started Feb 22, 2023 in Language design

78
You must be logged in to vote

Returning mutable references

utaal started Jan 19, 2022 in Language design

15
You must be logged in to vote

Consider disallowing body-less proofs that are not obligations

utaal started Jul 9, 2024 in Language design

0
You must be logged in to vote

Use when and make eager checking for spec fn requires configurable

utaal started Aug 23, 2023 in Language design

18
You must be logged in to vote

'returns' clause for exec functions

tjhance started Oct 11, 2023 in Language design

8
You must be logged in to vote

trusted/untrusted split

tjhance started Mar 27, 2022 in Language design

15
You must be logged in to vote

Chained conjunction forces spec mode

jonhnet started May 30, 2024 in Language design

3
You must be logged in to vote

favour an attribute style procedural macros

gilescope started May 5, 2024 in Language design · Closed

1
You must be logged in to vote

Import sets for ambient lemmas/axioms

utaal started Jan 20, 2022 in Language design

14
You must be logged in to vote

Proposal: rework the rules for old(self) in preconditions and postconditions

tchajed started Apr 18, 2023 in Language design

11
You must be logged in to vote

Using Verus from unverified client code

tjhance started Mar 24, 2022 in Language design

19
You must be logged in to vote

Ghostly DSTs

jaybosamiya started Feb 15, 2023 in Language design

1
You must be logged in to vote

Type invariants

tjhance started Jan 17, 2024 in Language design

4
You must be logged in to vote

Consider supporting assert (expression) by (spinoff)

utaal started Oct 30, 2023 in Language design

0
You must be logged in to vote

Partial functions / changes to recommends checking

utaal started Jul 14, 2023 in Language design · Closed

4
You must be logged in to vote

No analog of assert forall by for forall_arith; deprecate forall_arith?

jaylorch started Jun 12, 2023 in Language design · Closed

3
You must be logged in to vote

Allow top-level reveal in exec mode (without a proof block)

jaylorch started Apr 14, 2023 in Language design · Closed

5
You must be logged in to vote

Warn when declaring variables, parameters, and return values with a type with an incompatible mode

utaal started Jun 9, 2022 in Language design · Closed

2
You must be logged in to vote

Total spec closures and partial spec closures

Chris-Hawblitzel started Oct 3, 2023 in Language design

5
You must be logged in to vote

choose |x| P(x) should require exists |x| P(x)

jonhnet started Sep 6, 2023 in Language design · Closed

2
You must be logged in to vote

Consider using Into<int> on arguments in standard library function to not require manual casts

utaal started Sep 4, 2023 in Language design

0
You must be logged in to vote

Consider auto-importing the prelude for each module

utaal started Aug 23, 2023 in Language design

0

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Filter by label

Sorry, something went wrong.

Sorry, something went wrong.

No labels found. Sorry about that.

Categories

Language design Discussions

Supporting dyn soundly

Consider enforcing termination checking

Next-generation of Tracked/Ghost code

Improve error messages

Returning mutable references

Consider disallowing body-less proofs that are not obligations

Use `when` and make eager checking for spec fn requires configurable

'returns' clause for exec functions

trusted/untrusted split

Chained conjunction forces spec mode

favour an attribute style procedural macros

Import sets for ambient lemmas/axioms

Proposal: rework the rules for `old(self)` in preconditions and postconditions

Using Verus from unverified client code

Ghostly DSTs

Type invariants

Consider supporting `assert (expression) by (spinoff)`

Partial functions / changes to recommends checking

No analog of `assert forall by` for `forall_arith`; deprecate `forall_arith`?

Allow top-level `reveal` in `exec` mode (without a `proof` block)

Warn when declaring variables, parameters, and return values with a type with an incompatible mode

Total spec closures and partial spec closures

choose |x| P(x) should require exists |x| P(x)

Consider using `Into<int>` on arguments in standard library function to not require manual casts

Consider auto-importing the prelude for each module

verus-lang verus Language-design Discussions

Categories, most helpful, and community links

Categories

Community links

🗨️Language design Discussions

Language design Discussions