4 ms·
It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver
by hajile 4y ago
It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly.
Without such a theorem solver, it is all just "best practices" then hoping for the best.
- ducktective 4y agoIs there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?
- psd1 4y agocgi-bin
- mbrodersen 4y agoI am currently playing around with Dafny and it is very promising. I have use it to generate proven correct high-performance C# code without too much efforts. It’s great fun actually. Like a really cool puzzle game.