Discussions

• 2 You must be logged in to vote

  🗨️

  Improve error messages

  utaal started Feb 22, 2023 in Language design

  

  

  

  

  76
• 1 You must be logged in to vote

  💬

  Decouple context management from while loops

  jonhnet started Feb 14, 2024 in General

  

  

  

  

  6
• 1 You must be logged in to vote

  💬

  Uniformize lemma names in the standard library

  utaal started Aug 9, 2023 in General · Closed

  

  

  4
• 1 You must be logged in to vote

  💬

  copy & recursion checking

  tjhance started May 22, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  💬

  Address misleading diagnostics in --expand-errors

  utaal started Aug 27, 2023 in General

  

  

  

  

  5
• 1 You must be logged in to vote

  #️⃣

  Crucial rust/cargo features that are not supported

  panda2134 started May 20, 2024 in Feature requests

  

  

  3
• 1 You must be logged in to vote

  #️⃣

  About repeat expression in array

  zpzigi754 started May 17, 2024 in Feature requests · Closed

  

  

  2
• 1 You must be logged in to vote

  💬

  notes about variance

  tjhance started May 5, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  🗨️

  favour an attribute style procedural macros

  gilescope started May 5, 2024 in Language design · Closed

  

  

  1
• 4 You must be logged in to vote

  🗨️

  Import sets for ambient lemmas/axioms

  utaal started Jan 20, 2022 in Language design

  

  

  

  

  14
• 1 You must be logged in to vote

  💬

  Improve --verify-function and --verify-module

  utaal started Feb 21, 2023 in General

  

  

  4
• 1 You must be logged in to vote

  💬

  Consider using stable MIR at the top level of lowering HIR to VIR

  utaal started Apr 9, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  🗨️

  Supporting dyn soundly

  Chris-Hawblitzel started Mar 25, 2024 in Language design

  

  

  5
• 1 You must be logged in to vote

  💬

  Support multiple trait implementations for the same outer type

  jaybosamiya started Apr 9, 2023 in General · Closed

  

  

  

  

  7
• 3 You must be logged in to vote

  💬

  Support associated types with bounds

  marshtompsxd started Jun 26, 2023 in General · Closed

  

  

  2
• 1 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
• 1 You must be logged in to vote

  💬

  What's the best practice to combine verified code and original rust code?

  HaoYang670 started Aug 4, 2023 in General · Closed

  

  

  

  

  6
• 2 You must be logged in to vote

  🗨️

  Using Verus from unverified client code

  tjhance started Mar 24, 2022 in Language design

  

  

  

  

  19
• 1 You must be logged in to vote

  🗨️

  Ghostly DSTs

  jaybosamiya started Feb 15, 2023 in Language design

  

  

  1
• 1 You must be logged in to vote

  💬

  Replace fully axiomatic Seq with a model

  tchajed started Feb 15, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  🗨️

  Type invariants

  tjhance started Jan 17, 2024 in Language design

  

  

  4
• 1 You must be logged in to vote

  🗨️

  'returns' clause for exec functions

  tjhance started Oct 11, 2023 in Language design

  

  

  

  

  3
• 1 You must be logged in to vote

  💬

  Documentation improvements

  utaal started Nov 24, 2023 in General

  

  

  1
• 1 You must be logged in to vote

  💬

  Certificate error on play.verus-lang.org

  eminence started Nov 1, 2023 in General · Closed

  

  

  1
• 1 You must be logged in to vote

  💬

  Constants and arithmetic in bitvector assertions

  matthias-brun started Oct 25, 2023 in General

  

  

  

  

  4