3 ms·
> a fully-featured and usable (comparatively to today's personal computers) formally-specified... and proven computing system that goes from high-level language
by gavinpc 10y ago
> a fully-featured and usable (comparatively to today's personal computers) formally-specified... and proven computing system that goes from high-level language to operating system and application ecosystem to whatever machinery is used at the bottom.
The STEPS system from VPRI sounds like it checks most of those boxes. I don't think it's publicly available right now (although it was developed with NSF funding, so may eventually be).
http://www.vpri.org/pdf/tr2012001_steps.pdf http://www.vpri.org/pdf/tr2012001_steps.pdf
- panic 10y agoIs any part of STEPS formally specified? My understanding is that the goal of the project was to produce a system with a minimal volume of source code. Writing specifications alongside the source would make the project bigger, not smaller.