Thinking About Formal Verification Versus Formal Specification
You would think formal specification would be the one people do first, otherwise how do you compare different instances of what is being verified?
See
Geoffrey M. Brown Indiana University Bloomington | IUB - ResearchGate https://www.researchgate.net/profile/Geoffrey-Brown-3
Bryce Himebaugh's research works | Indiana University Bloomington ... https://www.researchgate.net/scientific-contributions/Bryce-Himebaugh-82112856
See Ben Eater's 8-bit computer https://eater.net/8bit/kits
Watch at least the first minute of the first video in the playlist:
See also the bit on the clock circuit at 16:07.
Now see: Verified Compilation on a Verified Processor https://cakeml.org/pldi19.pdf
As an exercise (thought experiment) consider how you might verify an 8-bit assembler on a verified 8-bit breadboard computer. What would that tell you about what you have achieved? How much is that knowledge worth, in practical terms?
In Bolivia I also had free access to the ISO/IEC specifications.
Computing in Phase Space
See Links:
- Ben Eater's 8-bit Breadboard Computer
- A 6502 Simulator Mystery Solved
- Emulating a 650 System in JavaScript
- 27c3: Reverse Engineering the MOS 6502 CPU (en)
The 6502 Song
See video description:
The 8 Bit Girls:
- AJ from @mydrunksibling
- Evie from @EviesRevue
- Veronica from @VeronicaExplains
- Jeri from @jeriellsworth
- Amy from @TiltFive
- Fuzzybad from https://itch.io/profile/fuzzybad
Lyrics:
There’s a joystick in my hand,
There’s Atari on the stand,
Put a cartridge in the slot,
‘cause we’re gonna play a lot,
There’s Atari on the stand,
Put a cartridge in the slot,
‘cause we’re gonna play a lot,
Switching on my Famicom
Cause Nintendo is the bomb
Mario’s the one I love,
Slipping on a power glove
Cause Nintendo is the bomb
Mario’s the one I love,
Slipping on a power glove
It’s an 8-bit world, and we’re 8-bit girls, it’s true, oh yeah
It’s an 8-bit world, and we’re 8-bit girls, it’s true, yeah
It’s an 8-bit world, and we’re 8-bit girls, it’s true, yeah
6502
Yeah we landed on the blocks, Space Invaders took some shots, then we ate up all the dots
6502
Frogger dodging all the cars, Breakout hitting all the bars, playing some Revenge of Yar
6502
Pole Position give me speed, Breaking up the Centipede, retrogames are what I need
6502
Yeah we’ve got the highest score, always say we want some more, more, whoa-oh
6502 microprocessor (x2)
Now I got this chip from MOS
Coding BASIC like a boss
This rf jack what’s it for?
Hooking up my Commodore
Coding BASIC like a boss
This rf jack what’s it for?
Hooking up my Commodore
Software on a floppy disk
Apple II cannot be missed
Want to see an epic fail?
Dysentery on the Trail.
Apple II cannot be missed
Want to see an epic fail?
Dysentery on the Trail.
6502! (x 8)
Comments
Post a Comment