diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6a2cae4..2c6b466 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+# Next
+
+- Add notations for format strings (`Format.t`)
+- `sprintf` and `sscanf` now take a format string of type `Format.t` instead of `string`
+- No longer compatible with 8.8 and 8.9
+
 # 1.0.1
 
 - Add `sscanf`
diff --git a/_CoqProject b/_CoqProject
index fd0b0ea..ae36bac 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,6 +3,8 @@
 theories/Flags.v
 theories/Digits.v
 theories/Format.v
+theories/FormatParser.v
+theories/FormatNotations.v
 theories/Justify.v
 theories/Printf.v
 theories/Scanf.v
diff --git a/test-suite/TestPrintf.v b/test-suite/TestPrintf.v
index 68d73e2..8d89249 100644
--- a/test-suite/TestPrintf.v
+++ b/test-suite/TestPrintf.v
@@ -2,6 +2,7 @@ Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import Coq.NArith.NArith.
 Require Import Coq.ZArith.ZArith.
+Require Import Printf.Digits.
 Require Import Printf.Printf.
 
 Local Open Scope string_scope.
diff --git a/theories/Digits.v b/theories/Digits.v
index 5562740..2782540 100644
--- a/theories/Digits.v
+++ b/theories/Digits.v
@@ -108,3 +108,18 @@ Definition string_of_digits (digit : N -> ascii) : digits -> string :=
 
 Definition string_of_N (base : N) (digit : N -> ascii) (n : N) : string :=
   string_of_digits digit (digits_of_N base n).
+
+Definition binary_string (n : N) :=
+  string_of_N 2 binary_ascii n.
+
+Definition hex_string (n : N) :=
+  string_of_N 16 hex_ascii n.
+
+Definition hex_string_upper (n : N) :=
+  string_of_N 16 hex_ascii_upper n.
+
+Definition octal_string (n : N) :=
+  string_of_N 8 octal_ascii n.
+
+Definition decimal_string (n : N) :=
+  string_of_N 10 decimal_ascii n.
diff --git a/theories/Format.v b/theories/Format.v
index 3c2c12e..8a0114c 100644
--- a/theories/Format.v
+++ b/theories/Format.v
@@ -4,30 +4,8 @@ Require Import Coq.NArith.NArith.
 Require Import Coq.ZArith.ZArith.
 Require Import Printf.Flags.
 
-(** ** Error handling in dependent types *)
-
-(** This tagged unit type indicates an error in the computation of a type. *)
-Variant tyerror {A : Type} (a : A) : Set := Invalid.
-
-(** Construct a dependent type from a computation which may fail. *)
-Definition for_good {E R : Type} (er : E + R) (k : R -> Type) : Type :=
-  match er with
-  | inl e => tyerror e
-  | inr r => k r
-  end.
-
-(** Apply a dependent function to the result of a computation when it is successful. *)
-Definition on_success {E R : Type} {er : E + R} {k : R -> Type} (f : forall r, k r)
-  : for_good er k :=
-  match er with
-  | inl e => Invalid e
-  | inr r => f r
-  end.
-
 (** ** String utilities *)
 
-Local Infix "::" := String : string_scope.
-
 Definition ascii_digit (c : ascii) : nat :=
   (if c =? "1" then 1
   else if c =? "2" then 2
@@ -80,118 +58,6 @@ Inductive t : Type :=
 | Hole : type -> options -> t -> t
 .
 
-Variant spec_state : Type :=
-| Flags
-| Width
-| TySpec (t : number_dectype)
-.
-
-(** Parser state machine. *)
-Variant state : Type :=
-| Ini                                  (* Initial state *)
-| Spec (j : spec_state) (o : options)  (* Parsing specifier *)
-  (* [j]: inner specifier parsing state *)
-  (* [o]: currently accumulated options *)
-.
-
-(** Parser error: dump the remaining string, that serves to locate the error. *)
-Variant error : Type :=
-| ErrorAt (i : state) (s : string)
-.
-
-Definition digit1to9 (c : ascii) : bool :=
-  (c =? "1")%char ||
-  (c =? "2")%char ||
-  (c =? "3")%char ||
-  (c =? "4")%char ||
-  (c =? "5")%char ||
-  (c =? "6")%char ||
-  (c =? "7")%char ||
-  (c =? "8")%char ||
-  (c =? "9")%char.
-
-Definition isFlagsOrWidth (j : _) : bool :=
-  match j with
-  | Flags | Width => true
-  | TySpec _ => false
-  end.
-
-Definition isWidth (j : _) : bool :=
-  match j with
-  | Width => true
-  | Flags | TySpec _ => false
-  end.
-
-Definition isFlags (j : _) : bool :=
-  match j with
-  | Flags => true
-  | Width | TySpec _ => false
-  end.
-
-(** Parse string [s] in state [i] into a format which is passed to the final
-  continuation [k], or return an error. *)
-Local Fixpoint parse_ {r : Type} (i : state) (k : t -> r) (s0 : string)
-  : error + r :=
-  match i, s0 with
-    (* The initial state looks for ["%"], indicating a specifier,
-       and keeps the rest as literal. *)
-  | Ini, ""%string => inr (k Empty)
-  | Ini, c :: s =>
-    if (c =? "%")%char then
-      let continue (_ : unit) := parse_ (Spec Flags default_options) k s in
-      match s with
-      | c' :: s =>
-        if (c' =? "%")%char then parse_ Ini (fun fmt => k (Literal "%" fmt)) s
-        else continue tt
-      | _ => continue tt
-      end
-    else
-      parse_ Ini (fun fmt => k (Literal c fmt)) s
-
-  | Spec _ _, ""%string => inl (ErrorAt i s0)
-  | Spec j o, a :: s =>
-    (* When parsing a specifier, the next character is either:
-       - a specifier character, then update the format and go back to the initial state;
-       - or a flag (or width) character, then update the options accordingly. *)
-    let specifier (t : type) := parse_ Ini (fun fmt => k (Hole t o fmt)) s in
-    let flag (j : spec_state) (o : options) := parse_ (Spec j o) k s in
-    let typ (t : number_dectype) := parse_ (Spec (TySpec t) o) k s in
-    let number b := Number b
-      match j with
-      | TySpec t => t
-      | _ => T_Nat
-      end in
-    if a =? "s" then specifier String
-    else if a =? "c" then specifier Char
-    else if a =? "b" then specifier (number Binary)
-    else if a =? "o" then specifier (number Octal)
-    else if a =? "d" then specifier (number Decimal)
-    else if a =? "x" then specifier (number HexLower)
-    else if a =? "X" then specifier (number HexUpper)
-    else if a =? "N" then typ T_N
-    else if a =? "Z" then
-      match j, s with
-      | (Flags | Width), c :: s => if c =? "d"%char then parse_ Ini (fun fmt => k (Hole SDecimal o fmt)) s
-        else inl (ErrorAt i s0)
-      | _, _ => inl (ErrorAt i s0)
-      end
-    else if ((digit1to9 a && isFlagsOrWidth j) || ((a =? "0")%char && isWidth j))%bool then
-      flag Width (update_option_width o (ascii_digit a))
-    else
-    match j with
-    | Flags =>
-      if a =? "-" then flag Flags (update_option_justify o LeftJustify)
-      else if a =? "+" then flag Flags (update_option_sign o true)
-      else if a =? " " then flag Flags (update_option_space o true)
-      else if a =? "#" then flag Flags (update_option_prefix o true)
-      else if a =? "0" then flag Flags (update_option_zero_pad o true)
-      else inl (ErrorAt i s0)
-    | _ => inl (ErrorAt i s0)
-    end
-  end%char%string.
-
-Definition parse : string -> error + t := parse_ Ini id.
-
 Definition dectype_type (t : number_dectype) : Type :=
   match t with
   | T_Nat => nat
diff --git a/theories/FormatNotations.v b/theories/FormatNotations.v
new file mode 100644
index 0000000..0a64603
--- /dev/null
+++ b/theories/FormatNotations.v
@@ -0,0 +1,12 @@
+(** * Notations for [Format.t] *)
+
+(** Reexport only the notations. *)
+
+Require Import Printf.Format.
+Require Import Printf.FormatParser.
+
+Declare Scope fmt_scope.
+Delimit Scope fmt_scope with fmt.
+Bind Scope fmt_scope with Format.t.
+
+String Notation Format.t parse_opt print : fmt_scope.
diff --git a/theories/FormatParser.v b/theories/FormatParser.v
new file mode 100644
index 0000000..a4864b9
--- /dev/null
+++ b/theories/FormatParser.v
@@ -0,0 +1,193 @@
+(** * Parse [string] to [Format.t] and print [Format.t] to [list Byte.byte] *)
+
+Require Import Coq.NArith.NArith.
+Require Import Coq.Strings.String.
+Require Import Coq.Strings.Ascii.
+
+Require Import Printf.Flags.
+Require Import Printf.Format.
+Require Import Printf.Digits.
+
+Local Infix "::" := String.String : string_scope.
+
+Import Format.
+
+Variant spec_state : Type :=
+| Flags
+| Width
+| TySpec (t : number_dectype)
+.
+
+(** Parser state machine. *)
+Variant state : Type :=
+| Ini                                  (* Initial state *)
+| Spec (j : spec_state) (o : options)  (* Parsing specifier *)
+  (* [j]: inner specifier parsing state *)
+  (* [o]: currently accumulated options *)
+.
+
+(** Parser error: dump the remaining string, that serves to locate the error. *)
+Variant error : Type :=
+| ErrorAt (i : state) (s : string)
+.
+
+Definition digit1to9 (c : ascii) : bool :=
+  (c =? "1")%char ||
+  (c =? "2")%char ||
+  (c =? "3")%char ||
+  (c =? "4")%char ||
+  (c =? "5")%char ||
+  (c =? "6")%char ||
+  (c =? "7")%char ||
+  (c =? "8")%char ||
+  (c =? "9")%char.
+
+
+Definition isFlagsOrWidth (j : _) : bool :=
+  match j with
+  | Flags | Width => true
+  | TySpec _ => false
+  end.
+
+Definition isWidth (j : _) : bool :=
+  match j with
+  | Width => true
+  | Flags | TySpec _ => false
+  end.
+
+Definition isFlags (j : _) : bool :=
+  match j with
+  | Flags => true
+  | Width | TySpec _ => false
+  end.
+
+(** Parse string [s] in state [i] into a format which is passed to the final
+  continuation [k], or return an error. *)
+Local Fixpoint parse_ {r : Type} (i : state) (k : t -> r) (s0 : string)
+  : error + r :=
+  match i, s0 with
+    (* The initial state looks for ["%"], indicating a specifier,
+       and keeps the rest as literal. *)
+  | Ini, ""%string => inr (k Empty)
+  | Ini, c :: s =>
+    if (c =? "%")%char then
+      let continue (_ : unit) := parse_ (Spec Flags default_options) k s in
+      match s with
+      | c' :: s =>
+        if (c' =? "%")%char then parse_ Ini (fun fmt => k (Literal "%" fmt)) s
+        else continue tt
+      | _ => continue tt
+      end
+    else
+      parse_ Ini (fun fmt => k (Literal c fmt)) s
+
+  | Spec _ _, ""%string => inl (ErrorAt i s0)
+  | Spec j o, a :: s =>
+    (* When parsing a specifier, the next character is either:
+       - a specifier character, then update the format and go back to the initial state;
+       - or a flag (or width) character, then update the options accordingly. *)
+    let specifier (t : type) := parse_ Ini (fun fmt => k (Hole t o fmt)) s in
+    let flag (j : spec_state) (o : options) := parse_ (Spec j o) k s in
+    let typ (t : number_dectype) := parse_ (Spec (TySpec t) o) k s in
+    let number b := Number b
+      match j with
+      | TySpec t => t
+      | _ => T_Nat
+      end in
+    if a =? "s" then specifier String
+    else if a =? "c" then specifier Char
+    else if a =? "b" then specifier (number Binary)
+    else if a =? "o" then specifier (number Octal)
+    else if a =? "d" then specifier (number Decimal)
+    else if a =? "x" then specifier (number HexLower)
+    else if a =? "X" then specifier (number HexUpper)
+    else if a =? "N" then typ T_N
+    else if a =? "Z" then
+      match j, s with
+      | (Flags | Width), c :: s => if c =? "d"%char then parse_ Ini (fun fmt => k (Hole SDecimal o fmt)) s
+        else inl (ErrorAt i s0)
+      | _, _ => inl (ErrorAt i s0)
+      end
+    else if ((digit1to9 a && isFlagsOrWidth j) || ((a =? "0")%char && isWidth j))%bool then
+      flag Width (update_option_width o (ascii_digit a))
+    else
+    match j with
+    | Flags =>
+      if a =? "-" then flag Flags (update_option_justify o LeftJustify)
+      else if a =? "+" then flag Flags (update_option_sign o true)
+      else if a =? " " then flag Flags (update_option_space o true)
+      else if a =? "#" then flag Flags (update_option_prefix o true)
+      else if a =? "0" then flag Flags (update_option_zero_pad o true)
+      else inl (ErrorAt i s0)
+    | _ => inl (ErrorAt i s0)
+    end
+  end%char%string.
+
+Definition parse : string -> error + t := parse_ Ini id.
+
+Definition parse_opt (s : list Byte.byte) : option t :=
+  match parse (string_of_list_byte s) with
+  | inl _ => None
+  | inr fmt => Some fmt
+  end.
+
+Local Open Scope list_scope.
+
+Definition print_options (opts : options) (etc : list Byte.byte) : list Byte.byte :=
+  let etc :=
+    match option_width opts with
+    | None => etc
+    | Some n => (list_byte_of_string (decimal_string (N.of_nat n)) ++ etc)%list
+    end in
+  let etc := if option_zero_pad opts then byte_of_ascii "0" :: etc else etc in
+  let etc := if option_prefix opts then byte_of_ascii "#" :: etc else etc in
+  let etc := if option_space opts then byte_of_ascii " " :: etc else etc in
+  let etc := if option_sign opts then byte_of_ascii "+" :: etc else etc in
+  match option_justify opts with
+  | LeftJustify => byte_of_ascii "-" :: etc
+  | RightJustify => etc
+  end.
+
+Definition print_type (ty : type) (etc : list Byte.byte) : list Byte.byte :=
+  match ty with
+  | Number enc dec =>
+    let enc_letter := byte_of_ascii
+      match enc with
+      | Binary => "b"
+      | Octal => "o"
+      | Decimal => "d"
+      | HexLower => "x"
+      | HexUpper => "X"
+      end in
+    match dec with
+    | T_Nat => enc_letter :: etc
+    | T_N => byte_of_ascii "N" :: enc_letter :: etc
+    end
+  | SDecimal => byte_of_ascii "Z" :: byte_of_ascii "d" :: etc
+  | String => byte_of_ascii "s" :: etc
+  | Char => byte_of_ascii "c" :: etc
+  end.
+
+Fixpoint print (fmt : t) : list Byte.byte :=
+  let pc := byte_of_ascii "%" in
+  match fmt with
+  | Empty => nil
+  | Literal c fmt =>
+    if (c =? "%")%char then pc :: pc :: print fmt
+    else byte_of_ascii c :: print fmt
+  | Hole ty opts fmt =>
+    pc :: print_options opts (print_type ty (print fmt))
+  end.
+
+Section Test.
+
+Let roundtrip (s : string) : Prop :=
+  match parse s with
+  | inl _ => False
+  | inr fmt => string_of_list_byte (print fmt) = s
+  end.
+
+Let roundtrip_test : roundtrip " %% %11d %+Nd %-Zd %x %NX %033s % #c".
+Proof. reflexivity. Qed.
+
+End Test.
diff --git a/theories/Printf.v b/theories/Printf.v
index 979df7d..6e3c0ae 100644
--- a/theories/Printf.v
+++ b/theories/Printf.v
@@ -8,6 +8,8 @@ Require Import Printf.Flags.
 Require Import Printf.Format.
 Require Import Printf.Digits.
 
+Require Export Printf.FormatNotations.
+
 Set Primitive Projections.
 
 Local Infix "::" := String : string_scope.
@@ -44,21 +46,6 @@ Definition prefix_string (o : options) (prefix : string) (n : N) (s : string) :
              s
   end.
 
-Definition binary_string (n : N) :=
-  string_of_N 2 binary_ascii n.
-
-Definition hex_string (n : N) :=
-  string_of_N 16 hex_ascii n.
-
-Definition hex_string_upper (n : N) :=
-  string_of_N 16 hex_ascii_upper n.
-
-Definition octal_string (n : N) :=
-  string_of_N 8 octal_ascii n.
-
-Definition decimal_string (n : N) :=
-  string_of_N 10 decimal_ascii n.
-
 (* helper methods to format *)
 Definition format_s
            (o : options)
@@ -131,7 +118,7 @@ Definition format (ty : Format.type)
   | Format.Char => fun o c => format_s o (c :: "")
   end.
 
-Local Fixpoint sprintf' (acc : string -> string) (fmt : Format.t)
+Fixpoint sprintf' (acc : string -> string) (fmt : Format.t)
   : Format.holes string fmt :=
   match fmt return Format.holes string fmt with
   | Format.Empty => acc ""%string
@@ -139,5 +126,5 @@ Local Fixpoint sprintf' (acc : string -> string) (fmt : Format.t)
   | Format.Hole ty o fmt => fun x => sprintf' (fun s => acc (format ty o x s)) fmt
   end.
 
-Definition sprintf (s : string) : for_good (Format.parse s) (Format.holes string) :=
-  on_success (sprintf' id).
+Definition sprintf (fmt : Format.t) : Format.holes string fmt :=
+  sprintf' id fmt.
diff --git a/theories/Scanf.v b/theories/Scanf.v
index d484b43..3f7fa6c 100644
--- a/theories/Scanf.v
+++ b/theories/Scanf.v
@@ -6,6 +6,8 @@ Require Import Printf.Justify.
 Require Import Printf.Flags.
 Require Import Printf.Format.
 
+Require Export Printf.FormatNotations.
+
 Set Primitive Projections.
 
 Local Infix "::" := String : string_scope.
@@ -273,18 +275,15 @@ Definition parse_hole (ty : Format.type) (o : options)
   | Format.SDecimal => parse_signed o
   end.
 
-Local Fixpoint parse_fmt (fmt : Format.t)
+Fixpoint sscanf (fmt : Format.t)
   : fmt_parser R fmt :=
   match fmt with
   | Format.Empty => fun k => k
   | Format.Literal c fmt => fun k =>
     if (c =? " ")%char
-    then parse_whitespace (fun _ => parse_fmt fmt k)
-    else parse_this_char c (fun _ => parse_fmt fmt k)
-  | Format.Hole ty o fmt => fun k => parse_hole ty o (fun x => parse_fmt fmt (k x))
+    then parse_whitespace (fun _ => sscanf fmt k)
+    else parse_this_char c (fun _ => sscanf fmt k)
+  | Format.Hole ty o fmt => fun k => parse_hole ty o (fun x => sscanf fmt (k x))
   end.
 
-Definition sscanf (s : string) : for_good (Format.parse s) (fmt_parser R) :=
-  on_success parse_fmt.
-
 End Parser.