Writing with tag

idris

• Formally verifying insertion sort in Idris

  May 24, 2026

  15 min

  idris

  dependent-type

  Using the dependently-typed programming language Idris to verify insertion sort.