If any of the attendees have another project they want publicised then reply to this mail, or let me know for next month and I’ll include it.
Notes from last meeting:
Attendees (6): Amos, Erik, Josh M, Josh P, Tran, Ben
Josh P: discussion of the Tako project he has started, which does Hoare logic style verification.
Amos: mentions Autocorres which was built as part of the seL4 project. AutoCorres takes C code that uses fixed width ints and tries to lift it to use unbounded Nats, which can make the proof easier. Also simplifies pointer arithmetic.
Josh P: mentions Coherent Extrapolated Volition as part of a conversation about AI risk. CEV seeks to instruct the AI model to “do what I want, not what I tell you”.
Amos: mentions the local organisation Gradient Institute which investigates AI risk locally in Sydney.
Erik: mentions Project Veritas whistleblowing organisation, which investigates issues like ML algorithms that are set up in a way to achieve particular political outcomes.
Josh P: mentions Synquid program synthesiser based on refinement types, a MIT project.
Amos: experimenting with program generation via tactics, trying to get Coq tactics to generate a desired computational program from its type.