Bit different though! In your example, the video is made from manually syncing with the song bpm, as the beep is at a constant rate. It's basically just a hand-made visualization of (every other) kick drum.
While the submission has the notes not at a basic 1/4 tempo, and is automatically "animated" based on the constrained optimization. Also leads to a much more interesting visualization :)
Note that "CheerpX enables you to run existing 32-bit x86 native binaries".
For some reason support for wasm64 (in browsers) has been stagnated for years, which is a pity.
They should compare with other multithreading and GPU approaches for SAT/SMT solving (like https://www.win.tue.nl/~awijs/articles/parafrost_gpu.pdf from Armin Biere, or other works from Mate Soos). There has been a lot of research in this direction.
WASM is an extremely useful compilation target because of its portability (specially for running on browsers), but it is far from being the "default compilation target" for almost any language. The promised near-native speed is not here (in general you get x2 or x3 slower code but it can be even worse), it is limited to 32-bits (MEMORY64 is on the way but there is not a clear roadmap of when this will be generally available in browsers), blocking IO is a pain, and its design seems to be constrained by the underlying JS JIT (it still looks like ASM.JS with a different syntax).
I still believe that it is a miracle that we have WASM as a standard, and that it runs smoothly across different browser vendors, but why nobody seems to be worried about lack of progress in performance?
LLVM IR would be a much better binary target. It was used in the abandoned PNaCL project. AFAIK Apple uses it (bitcode) to store apps that are later compiled for specific platforms. WASM looks like a toy compared with this technology.
I worked on PNaCl back in 2011. There was a growing understanding that choosing LLVM IR as the representation was a mistake. I even tried to come up with something better, but failed to do so. I was glad to see asm.js and then WebAssembly coming to the scene. In my opinion, WebAssembly is better than what PNaCl could have ever become.
The problem is that LLVM IR makes breaking changes fairly frequently -- for instance, LLVM 15 made all pointers untyped; where before you'd have a type like *i32, now you just have ptr.
If you're trying to run the same IR on 32-bit and 64-bit devices, I'd expect you'd need to freeze the word size anyway -- if a C or C++ program uses sizeof(), what value gets returned?
Blocking IO doesn't get solved by switching to LLVM either; you can't block in browser WASM because it'd block the JS thread; a WASM engine not attached to a browser has no such issues. (I wish at least one-shot continuations would get added so that this could become a bit easier in the browser, but I understand the hesitancy to do so...)
Surprisingly it can generate Coq proofs. Unsurprisingly the "proofs" are just hallucinations that look right but make no sense at all. See for example: "coq program that proves that p->q is equivalent to q->p", which produces:
That has been my experience for all my attempts of using chatgpt for any programming tasks: ask it something contained in the first stackoverflow answer when you google your prompt, and sure enough it gives you that. But ask it for something slightly more involved and you get something that looks plausible at very first glance but is just pure junk.
My impression when working with people using Simulink is that 'safety' is much weaker that for people working on formal methods, and certification limited a lot the kind of programs that they would write. It made totally sense for their domain, but -- as a general practice to write software -- it didn't impress me at all. I may be wrong.
I was expecting functional safety standards to require the use of formal methods, similar for example to how AWS uses TLA+, but I was surprised to discover it was not a requirement at all.
The general term of arithmetic and geometric sequences seem simpler when indexing from 0 rather than 1. I do not think that '1' is more human focused for anything than '0'.
