← Back to context

Comment by westurner

8 months ago

OTOH feature ideas: Formal Verification, Process Isolation, secure coding in Rust,

- Quark is written in Coq and is formally verified. What can be learned from the design of Quark and other larger formally-verified apps.

From "Why Don't People Use Formal Methods?" (2019) https://news.ycombinator.com/item?id=39046787 :

>> What are some ideas for UI Visual Affordances to solve for bad UX due to slow browser tabs and extensions?

>> - [ ] UBY: Browsers: Strobe the tab or extension button when it's beyond (configurable) resource usage thresholds

>> - [ ] UBY: Browsers: Vary the {color, size, fill} of the tabs according to their relative resource utilization

>> - [ ] ENH,SEC: Browsers: specify per-tab/per-domain resource quotas: CPU

- What can be learned from few methods and patterns from rust rewrites, again of larger applications

"MotorOS: a Rust-first operating system for x64 VMs" https://news.ycombinator.com/item?id=34743393

> [Rust Secure Coding Guidelines, awesome-safety-critical,]