Is 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?
I 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.
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?