We're probably on the same page about formal methods.
I wanted to point out a cool example I helped with: formalizing the structured control flow rules for SPIR-V.
https://dl.acm.org/doi/10.1145/3571253
This was a really nice blend of theory and practice to nail the details on a gnarly bit of the GPU intermediate language we know and love. And in the end the (prose) rules are easier to understand too.
There are now 48 registered SPIR-V generator tools.
Woohoo.
https://github.com/KhronosGroup/SPIRV-Headers/blob/main/include/spirv/spir-v.xml#L100
I'm getting the material ready for my upcoming #GPGPU course that starts on March. Even though I most probably won't get to it,I also checked my trivial #SYCL programs. Apparently the 2025.0 version of the #Intel #OneAPI #DPCPP runtime doesn't like any #OpenCL platform except Intel's own (I have two other platforms that support #SPIRV, so why aren't they showing up? From the documentation I can find online this should be sufficient, but apparently it's not …)
I've been writing quite a few SPIR-V modules by hand for testing lately. It's tolerable, but only barely.
My primary complaints are:
1. Verbosity. A test for a single instruction tends to be at least 20 lines and sometimes much more.
2. SSA is great for compilers, not so much for humans.
3. Getting all of the type declarations and capabilities right is annoying.
Is there a better way? #spirv
Vulkan 1.4:
Glslang, Shaderc, and SPIRV-Tools updates have landed to be able to target Vulkan 1.4.
No major changes to Vulkan SPIR-V, so this is mostly about being able to specify Vulkan 1.4 in options lists.
These will be rolled into the next Vulkan SDK.
The rust-gpu project now has two more maintainers. Happy to see the project gaining speed!
I'm using rust-gpu for most my Vulkan experiments these days. It's one of the enablers of my SDF-compiler toolchain. It lets you define linking points, which in turn allows me to link my SDF generated SPIR-V code into rust-gpu generated SPIR-V modules.
I think people get tied up in knots when trying to parse SPIR-V with structured control flow.
You gotta do it in reverse structured post-order.
Once you lay out the basic blocks in that order, the nested control constructs map to *intervals* over that list. (:galaxy brain:)
For details, see Tint's SPIR-V to WGSL translator.
@ypujante
(And, those would be one of the unit tests of the SPIR-V to WGSL translator, converted to an end-to-end test so we can check the right thing will be emitted on all the backend languages.)
I know SPIR-V is not meant for human readability and all that, but damn. Is there not any way that the variables were named anything closer to useful than %13525? I understand that it's not a one-to-one match with my glsl variables, but like... This feels like it's actively trying to obfuscate the code 
Maybe there's some glslang option I don't know about that tries to make them a bit clearer?
