Notes from meeting 10/9/2019
Attendees (4): Erik, Josh M, Richard, Ben.
Ben and Josh attended ICFP in Berlin. Notable papers: Agda extension for Cubical Type Theory. Typed Holes in GHC. Lennart Augustsson and Satnam Singh gave a good talk about use of GHC/Haskell in their project at X. Several groups are now looking at verifying properties of neural networks.
Next year’s ICFP is in New Jersey, then Seoul in 2021, then Slovenia in 2022.
Erik: working on the backend for the Cardano block explorer. Has had good experiences with the persistent and esqueleto Haskell libraries.
Josh: working on extensible .hi files for GHC, so more information can be stored in them to aid cross compilation.
Josh: went to the Cardano meetup while Berlin. Showed a ‘Tangem’ crypto wallet card that holds the private key in a secure IC and can be used to sign transactions. The private key cannot be retrieved from the hardware without destroying the IC. To perform transactions one can simply give someone else the card.
Erik: private transactions are now increasingly being done using Monero instead of the other currencies. US agencies have been blacklisting certain Bitcoin(etc) addresses and exchanges will not take any coins that have been coin joined with the blacklisted coins. Bitcoins ‘pseudo anonymity’ has ceased being good enough for private transactions.
Ben: has been testing out the Why3 prover framework for proving properties about image processing algorithms. Programs are written in a simple dialect of ML called WhyML, which includes preconditions and postconditions for functions (using the ‘requires’ and ‘ensures’ keyword). Intermediate verification goals can be farmed out to a range of SMT solvers including Alt-Ergo, CVC4 and Z3. The experience has been good so far. The framework uses first order logic so one cannot parameterise properties by other properties, but the SMT solvers are good at handling the sort of statements about array indexing you get when verifying image processing algorithms.
Notes from earlier meeting of 6/8/2019
Attendees (4): Amos, Erik, Richard, Ben.
Richard / Amos: have been reading about Barry’s Closure Calculus (from the paper A Simpler Lambda Calculus). Amos did a formalisation in Isabelle and agrees that it’s easier to formalises than lambda calculi using traditional approaches to substitution.
Erik: writing a blockchain explorer for Cardano. The backend uses Postgres domain types to help ensure the data stays well formed. The domain types are like static refinement types, except they are checked at runtime.
Erik: mentions Zether, a new mechanism for performing private transactions on the main Ethereum blockchain.
Ben: joined Ghost Locomotion along with Amos, Tran and Kai. Have been reading about SPIR language for GPGPU programming, and writing some simple examples in OpenCL to get familiar with the API. Also reading about the various weak memory models exposed by OpenCL and other languages.
Erik: describes fuzz testing of libsndfile using the American Fuzzy Lop fuzz testing framework. Found ~30 bugs in 3-4 days of fuzzing, which is more than have been found in the last 15 years of production use as a well used open source library.
Ben: started reading about verification of neural networks. Amos mentions recent work on placing bounds on the output of a neural network. Propagates bounds backwards using an SMT solver.