Top 1,000 Features Creators Events Podcasts Extensions Blog Explorer CSV Download


< >

Low* is a programming language created in 2008.

#2317on PLDB 16Years Old

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 ()

View source

- Build the next great programming language · About · Resources · Acknowledgements · Part of the World Wide Scroll