Low* - Programming language

Low* is a programming language created in 2008.

#2272on PLDB

16Years Old

Tags: programming language
Early development of Low* happened in Microsoft and Inria
Low* compiles to C
First announcement of Low*

Example from the web:

let chacha20
 (len: uint32{len ≤ blocklen})
 (output: bytes{len = output.length})
 (key: keyBytes)
 (nonce: nonceBytes{disjoint [output; key; nonce]})
 (counter: uint32) : Stack unit
 (requires (λ m0 → output ∈ m0 ∧ key ∈ m0 ∧ nonce ∈ m0))
 (ensures (λ m0 _m1 → modifies1 output m0 m1 ∧
 m1.[output] ==
  Seq.prefix len (Spec.chacha20 m0.[key] m0.[nonce]) counter))) =
  push_frame ();
  let state = Buffer.create 0ul 32ul in
  let block = Buffer.sub state 16ul 16ul in
  chacha20_init block key nonce counter;
  chacha20_update output state len;
  pop_frame ()