Recently I have been using SPARK and it's a pretty different development mindset than the embedded C that I had been used to. It makes me wonder if other devel

Recently I have been using SPARK and it's a pretty different development mindset than the embedded C that I had been used to. It makes me wonder if other development areas could benefit from adopting some of this mindset and discipline. For example, just to take a random example of Java or Python, what would it look like to create a strict subset of language features which allowed for formally provable code and to create a static analysis tool which could achieve it. I realize that this sort of thing isn't for many developers or many sorts of projects. However, I would like to see more folks taking the best parts of High Integrity Software development and bringing it out to the wider world.