It doesn't answer some obvious questions I have though:
1. What are the limitations? Presumably it doesn't work with assembly, external C libraries etc. What about unsafe code? Traits? Heap allocation? Threads? Etc.
2. How is this different to other projects, e.g. Kani? Kani uses the CBMC checker which can use a variety of SMT solvers. IIRC symbol execution is a different approach to SMT solving but I can't remember the details. What practical impact does it have?
Also, crappy only applies if you insist on using the wrong device for viewing them (pro tip: don't use a phone). Otherwise, the experience is superior.
You will need a display that can show the full page comfortably, that is true, but a 27inch monitor or a large iPad will do.
I'd prefer something more flexibel than PDF as well, but all alternatives compromise on quality and/or ease of use. There seems to be no market for good looking digital documents other than PDF.
I think it's because I am not used to reading academic papers, so I don't know how to read the paper or where to get started. Do I start from top to bottom? Those papers get quite big so I don't think that's the right approach, they also tend to get very meaty with the keywords so I end up reading the same sentence multiple times because I have to lookup every word or try to grasp the concept they are explaining. Maybe I should start with the abstract first? I don't know.
Top to bottom is usually the best way to go, especially read first abstract & introduction, but don't be afraid to skip sections if they seem unclear or you just don't understand what they are trying to tell you.
These days, you could put the paper into NotebookLM, and generate a podcast, that will generate something friendly, but might be partially wrong or skip over essential stuff.
