Home | Blog | Wiki | About

[2024-03-11 Mon]

• cc hack: Brian Kernighan shows how a compiler can inject backdoors to allow root logins (1984?) ʳ
• Major systemʷ: a way to remember numbers by thinking of them as words corresponding to sounds.

[2024-02-22 Thu]

• Disagreement between Hilbert and Brouwer ʷ
• GeoCoq: An attempt to formalize (Euclidean?) geometry in Coq
• hack: 'PHP with types'. Made at facebook/meta ʳ
  • HHVM: HipHop Virtual Machine
  • Written mostly in OCaml (also uses js_ofocaml??)
  • https://github.com/facebook/hhvm/tree/master/hphp/hack

[2024-02-16 Fri]

• Importance of formal verification: A blog post at Formal Land

[2024-02-15 Thu]

• A tiny introduction to lens (Haskell library) as a tutorial: link

[2023-11-01 Wed]

• More fixpoints! (Functional pearl): https://dl.acm.org/doi/10.1145/3607853
  • https://github.com/nomeata/haskell-rec-def
• About a way of removing left-recursion in grammars: https://www.joachim-breitner.de/blog/807-Left_recursive_parser_combinators_via_sharing

[2023-10-27 Fri]

• https://research.swtch.com/nih
• Delimited continuations
  • Returns a value and hence can be reused, unlike the 'usual' continuations

[2023-10-14 Sat]

• The stacks project: An online collaborative textbook about algebraic geometry
• Bloom filter
• Kansas Lava: An implementatation Lava, the Haskell eDSL for hardware design
• Dancing links: Data structure?

[2023-10-09 Mon]

• Default logicʷ

[2023-10-03 Tue]

• SECD machineʷ: An abstract machine specifically intended to evaluate lambda calculus expressions

[2023-09-28 Thu]

• Etymology of the 'liquid' in liquid types (as in Liquid haskell) is 'Logically Qualified'
  • From PLDI'08 ᵖ
  • Original implementation seems to have been in OCaml.