diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2024-07-07
+        * Version bump (3.20). (#522)
+        * Remove deprecated function Copilot.Language.Spec.forall. (#518)
+        * Add support for struct field updates. (#520)
+
 2024-05-07
         * Version bump (3.19.1). (#512)
 
diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             3.19.1
+version:             3.20
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -35,16 +35,16 @@
 library
   default-language: Haskell2010
   hs-source-dirs: src
-  build-depends: base                  >= 4.9    && < 5
+  build-depends: base                  >= 4.9  && < 5
 
-               , array                 >= 0.5    && < 0.6
-               , containers            >= 0.4    && < 0.7
-               , data-reify            >= 0.6    && < 0.7
-               , mtl                   >= 2.0    && < 3
+               , array                 >= 0.5  && < 0.6
+               , containers            >= 0.4  && < 0.7
+               , data-reify            >= 0.6  && < 0.7
+               , mtl                   >= 2.0  && < 3
 
-               , copilot-core          >= 3.19.1 && < 3.20
-               , copilot-interpreter   >= 3.19.1 && < 3.20
-               , copilot-theorem       >= 3.19.1 && < 3.20
+               , copilot-core          >= 3.20 && < 3.21
+               , copilot-interpreter   >= 3.20 && < 3.21
+               , copilot-theorem       >= 3.20 && < 3.21
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/src/Copilot/Language.hs b/src/Copilot/Language.hs
--- a/src/Copilot/Language.hs
+++ b/src/Copilot/Language.hs
@@ -38,7 +38,7 @@
   , prop
   , theorem
   , forAll
-  , forall, exists
+  , exists
   ) where
 
 import Data.Int hiding (Int)
diff --git a/src/Copilot/Language/Operators/Struct.hs b/src/Copilot/Language/Operators/Struct.hs
--- a/src/Copilot/Language/Operators/Struct.hs
+++ b/src/Copilot/Language/Operators/Struct.hs
@@ -1,8 +1,35 @@
 {-# LANGUAGE Safe #-}
 
 -- | Combinators to deal with streams carrying structs.
+--
+-- We support two kinds of operations on structs: reading the fields of structs
+-- and modifying the fields of structs.
+--
+-- To obtain the values of field @x@ of a struct @s@, you can just write:
+--
+-- @
+-- expr = s # x
+-- @
+--
+-- If you want to update it, use instead a double hash to refer to the field.
+-- You can either update the field:
+--
+-- @
+-- expr = s ## x =: 75
+-- @
+--
+-- To update it by applying a function to it, for example, the function that
+-- updates a stream by one unit, just do:
+--
+-- @
+-- expr = s ## x =$ (+1)
+-- @
 module Copilot.Language.Operators.Struct
   ( (#)
+  , Projection
+  , (##)
+  , (=:)
+  , (=$)
   ) where
 
 import Copilot.Core.Type
@@ -18,6 +45,46 @@
 -- of type @Word8@, and @s@ is a stream of type @Stream T@, then @s # t2@ has
 -- type @Stream Word8@ and contains the values of the @t2@ field of the structs
 -- in @s@ at any point in time.
-(#) :: (KnownSymbol s, Typed t, Typed a, Struct a)
-      => Stream a -> (a -> Field s t) -> Stream t
+(#) :: (KnownSymbol f, Typed t, Typed s, Struct s)
+      => Stream s -> (s -> Field f t) -> Stream t
 (#) s f = Op1 (GetField typeOf typeOf f) s
+
+-- | Type represented an unapplied struct field accessor and a stream carrying
+-- structs.
+data Projection s f t = Projection (Stream s) (s -> Field f t)
+
+-- | Pair a stream with a field accessor, without applying it to obtain the
+-- value of the field.
+--
+-- This function is needed to refer to a field accessor when the goal is to
+-- update the field value, not just to read it.
+(##) :: (KnownSymbol f, Typed t, Typed s, Struct s)
+     => Stream s -> (s -> Field f t) -> Projection s f t
+(##) = Projection
+
+-- | Create a stream where the field of a struct has been updated with values
+-- from another stream.
+--
+-- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@
+-- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and $sT1$
+-- is a stream of type @Int32@ then @s ## t2 =: sT1@ has type @Stream T@ and
+-- contains structs where the value of @t1@ is that of @sT1@ and the value of
+-- @t2@ is the value that the same field had in @s@, at any point in time.
+infixl 8 =:
+(=:) :: (KnownSymbol f, Typed t, Typed s, Struct s)
+     => Projection s f t -> Stream t -> Stream s
+(=:) (Projection s f) v = Op2 (UpdateField typeOf typeOf f) s v
+
+-- | Create a stream where the field of a struct has been updated by applying a
+-- function to it.
+--
+-- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@
+-- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and $f$ is
+-- a function from @Stream Int32 -> Stream Int32@ then @s ## t2 =$ f@ has type
+-- @Stream T@ and contains structs where the value of @t1@ is that of @f@
+-- applied to the original value of @t1@ in @s@, and the value of @t2@ is the
+-- value that the same field had in @s@, at any point in time.
+infixl 8 =$
+(=$) :: (KnownSymbol f, Typed t, Typed s, Struct s)
+     => Projection s f t -> (Stream t -> Stream t) -> Stream s
+(=$) (Projection s f) op = s ## f =: (op (s # f))
diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs
--- a/src/Copilot/Language/Spec.hs
+++ b/src/Copilot/Language/Spec.hs
@@ -28,7 +28,7 @@
   , prop, properties
   , theorem, theorems
   , forAll
-  , forall, exists
+  , exists
   , extractProp
   , Universal, Existential
   ) where
@@ -164,11 +164,6 @@
 -- | Universal quantification of boolean streams over time.
 forAll :: Stream Bool -> Prop Universal
 forAll = Forall
-
-{-# DEPRECATED forall "Use forAll instead." #-}
--- | Universal quantification of boolean streams over time.
-forall :: Stream Bool -> Prop Universal
-forall = forAll
 
 -- | Existential quantification of boolean streams over time.
 exists :: Stream Bool -> Prop Existential