Відео

really nice talk! it's an interesting perspective for what it means to make a compiler and an instruction set

Starts at - 43:20 Type Inference in OCaml and GHC using Levels - 1:47:00 Towards Generic Higher-Order Unification Implementations in Haskell - 2:45:00 Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax - 3:07:30 McTT Building A Correct-By-Construction Proof Checker For Martin-Löf Type Theory - 3:46:50 Eta conversion for the unit type (is still not that simple) - 6:14:50 Type Checking ~is~ Proof Reductions in Classical Linear Logic - 6:41:35 Incremental Bidirectional Typing via Order Maintenance - (several talks were not recorded)

Session 1 - 41:58 Keynote (audio from 54:15) Session 2 - 2:44:15 Helping users to reduce Brittleness in their Dafny programs - a success story - 3:06:11 Towards Proof Stability in SMT-based Program Verification - 3:22:28 Verifying the Fisher-Yates Shuffle Algorithm in Dafny - 3:41:51 Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems - 4:02:31 Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Session 3 - 5:28:25 Baking for Dafny: A CakeML Backend for Dafny (partial) - 5:45:02 Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean - 6:07:32 Performant, Readable and Interoperable Rust from Dafny - 6:25:19 Randomised Testing of the Dafny Compiler: Into the CI - Teaching Types and Non-Interference in Dafny (requested not to be streamed) Session 4 - 7:20:35 Laurel: Unblocking Automated Verification with Large Language Models - 7:41:35 VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search - 8:02:55 dafny-annotator: AI-Assisted Verification of Dafny Programs - 8:30:18 DafnyBench: A Benchmark for Formal Software Verification - 8:49:04 Dafny as Verification-Aware Intermediate Language for Code Generation - 9:05:05 Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

please there is No Sound :( :( from the video "Solvers, unite! A simple unified semantics for reasoning with assurance and agreement"

audio available from 54:15

Thank you :)

perhaps linked lists _did_ exist in the Cretaceous Era and cavedevs needed to reverse them, to elude dinosaurs. _(Perhaps.)_ But the point is that they do not exist _now_ and knowing how to reverse them by rubbing a stick rapidly in the center of some tinder is not a useful skill. We should not be “doomsday preppers” pretending we really need that linked list skill in the event society collapses and we’re all going to build the Internet from rocks and sticks again. When you use your Ph.D. in Applied Physics to interview for a job in semiconductor engineering, do they make you build a fire? No. Because it’s not relevant to the job. (In fact if you are _good_ at starting fires, you should probably be placed on a law enforcement watch list.) Anybody _sane_ would respond to the “can you build a fire” question in the semiconductor interview as some kind of cruel, bizarre hazing ritual. What’s next? Walking on coals? Being tattooed with the corporate logo on my forehead, to show I’ve been accepted into the tribe? Or [shudder] a trust exercise? no, linked lists do not exist, and any company that asks you to reverse one should be given the berth normally reserved for a vessel flying both the Jolly Roger 🏴‍☠️ and the “My ship has norovirus and plague and the rats are dying” flags.

but linked lists _must_ be real. how else do we explain UA-cam comments not having a tree structure

Scheme programming should be defun! * flame war follows *

Scheme-like languages has finally shaken off the joke about Soviet spies stealing Lisp ))))))))))))))))))))))))))))) code.

I'm just going to learn about this and I'm getting interested and I would like to be a master on this

24:00 what about when the increment causes an overflow? The invariant will be violated

Re: the question asking if there's a way to do intermutability: yeah, raw pointers.

I think the biggest barrier to user modifiable software today is that the target market is perhaps less than 2% of the consumer market. So there isn’t a huge demand for companies like Apple to create such software. However, I do think that user modifiable is necessary and inevitable, but certainly has challenges.

This is really important work. I've spent the year beating my head against provers, and I'm now really convinced by their power but the initial learning curve is so steep

This is the wrong talk!

我如何从钱包中将我的 89 USDT TRC20 提现到币安请帮帮我 12个钱包恢复短语：《pride》-《pole》-《obtain》-《together》-《second》-《when》-《future》-《mask》-《review》-《nature》-《potato》-《bulb》

Incredible work, must have been tough to do all that formalization!

Sound is lost until 4:35

Sound gets fixed at the 9 min mark.

Amazing presentation! Amazing contributions!

Fil-C, if performance is not your problem, you already have many options. It could be nice to 'just port' existing code in non-time critical parts without a total - rewrite in a different language. But most of those have already been re-written, so not sure about it

It's always a fun jumpscare when SPJ is in the audience and asks a question lol

I saw this video after getting plag in 3 out of 5 assignments😭😭😭

As someone who have dabbled in compiler development, I find the Rustlantis talk at 5:40:55 really interesting. If I'll ever want to make my crappy toy compiler with similarly SSA-based IR "production-ready", I'll make sure to use something like that to test it.

Super low sound volume

Great analysis, thank you! I need some advice: My OKX wallet holds some USDT, and I have the seed phrase. (alarm fetch churn bridge exercise tape speak race clerk couch crater letter). Could you explain how to move them to Binance?

No sound when a slide splash-fills the screen. It's back when we see Simon but it's the smaller part of the video 😢

do not waste your time on this video!

Sadly the code in this video is so dark and blurry it's impossible to make it out. Surely in 2024 we could get this right?

Do you insist on calling it Fil-C?

Fil-C: interesting, the 2x slowness would be critical for some projects

Very nice lecture about embedded domain specific languages. Some of the problems listed in the lecture like clear error messages and localization are already solved in the Ring programming language.

I'm a fan of this work, thanks for the updates 🙏🏻 Have you heard about Wiring Diagrams from Category Theory?

Good job

Fil-C: The idea of safe-memory C sounds good per se, but.. unfortunately it's too WIP. Trying to compile small programs leads to many errors like: In file included from "llvm-project-deluge/build/bin/../../pizfix/include/dirent.h:18: /usr/include/x86_64-linux-gnu/bits/dirent.h:25:5: error: unknown type name '__ino_t'; did you mean 'ino_t?", and many others. Then you have no idea what to do if there's no forum to discuss, no people who have worked with it and can share compat issues, and so on.

Image having all the functionality of like fnm, nvm, npm, pnpm, prettier, tsc, jest, test runner, doc building, etc., in one single tool... A true unified platform experience! Almost like cargo for Rust, but more. It's like what projects like Rome/Biome, etc., are just starting to do for the JS world... If this kind of tooling comes to OCaml, it might become my favorite tool to write projects.

The lecture looks very interesting! Unfortunately, this video has pretty bad audio. I'm wondering, is there any chance for a re-uploading with a better quality or is it lost in time?

blub

Awesome talk, Mark!

Very interesting

quite cool! accidentally diving down the DreamCoder rabbithole on a Saturday afternoon, and this seems much more runnable on my laptop

Really appreciated this.

Sound quality is horrible. Any chance you have a better audio lying around? Or subtitles?

0:50 Quick note that nobody is ever going to read: Even if everybody in the audience knows what "CSR" means (Compressed Sparse Rows?), the talk maybe later be watched by people only who have no idea, so it's still worth throwing out a quick slide.

whoa

Beautifully described. This is super awesome

31:42 Welcome & Opening (Peter van Hardenberg, Geoffrey Litt, Joshua Horowitz) 38:03 Keynote: The Meaning of LIVE (Jonathan Edwards) 1:24:56 Definitions and Dimensions of Liveness (Joshua Horowitz) Block 1: Visual Systems 2:31:30 Subsequently: Telling stories with pictures makes programs (Marcel Goethals) 2:45:00 Code flow canvas - a generic visual programming system (Maikel van de Lisdonk) 2:55:45 Snappets: a VR animation system based on Projective Geometric Algebra (Hamish Todd) 3:13:27 Inkling: Sketching Dynamic Systems (Marcel Goethals, Alessandro Warth, Ivan Reese) 3:28:48 Arroost: Unblocking creation with friends (Lu Wilson) 3:47:48 Q&A Block 1 Block 2: Textual Systems 5:34:22 Run, Build and Grow Small Systems Without Leaving Your Text Editor (Albert Zak, Karl M. Göschka) 5:49:06 TAPE: From direct to programmatic and back (Ian Clester) 6:05:17 Diff-based interactive compiler debugging and testing (Luyu Cheng, Lionel Parreaux) 6:16:06 Example-driven development: bridging tests and documentation (Oscar Nierstrasz, Andrei Chiş, Tudor Gîrba) 6:26:27 Live Programming a Live Programming Environment: An Experience Report (Elliot Evans, Philippa Markovics, Martin Kavalar, Andrea Amantini, Jack Rusher) 6:41:58 Q&A Block 2 Block 3: Substrates 7:34:15 Manifold: Throwing Together Software Systems (Jeff Lindsay) 7:49:40 EYG a predictable, and useful, programming language (Peter Saxton) 7:58:08 DocuApps: Ampleforth Documents as Applications (Gilad Bracha) 8:05:47 ScrapSheets: Async Programs in a Reactive 2D Environment (Taylor Troesh) 8:14:21 Scoped Propagators (Orion Reed) 8:24:02 Q&A Block 3 8:43:08 Closing & Farewell (Peter van Hardenberg, Geoffrey Litt, Joshua Horowitz)

Very entertaining talk!

Great speach, Federico Cassano 👏🏻👏🏻👏🏻