Alright, this sub-thread started with a person wondering if one could make C programs memory-safe against common errors. You replied with formal verification while I replied with automated tools that make C memory safe. One or two use formally-verified models. :) You countered with the needs of embedded making such tools impractical. There's many in that industry that can use tooling like I recommended, esp if not BOM-sensitive or hard real-time. You brought up the needs of ultra-constrained market in terms of cost or hard real-time. The increasing market-share of expensive ARM's vs 8-16-bitters and embedded JVM's makes me wonder if that's oversimplified, too. Makes me think similar companies might consider tooling like I described if it likewise adds benefit with tiny costs. The majority will do as you say and avoid these tools since they don't fit their use case. So will some non-embedded sectors focused only on performance or lowest cost.

Let's cut to some important stuff, though, as I think the argument got over semantics or at least less interesting stuff. My background is high-assurance security with generalist experience but none with formal methods or building static analyzers. You seem to have experience in those I don't. Appel, who makes the tool you linked, is a formal methodist (among other things) building stuff that's useful, achieves high-end stuff, and sometimes enabling less-skilled people. Rare type of researcher and deliverables I love seeing. You say you want to do something similar. So, let's have a more interesting conversation.

"Also, Astree isn't free software. It's an AbsInt product" (and CompCert)

I saw writing on wall with CompCert when they hesitated to FOSS it or answer questions. So sad such a wonderful tool got locked up. Thanks for confirming with a dollar range what I suspected. Same with Astree. We need replacements for both like you said about CompCert. My first idea was for a team to clone CompCert based on high-level description of what it does with dependent types a la Chlipala or just FLINT ML-style compiler. Add Design-by-Contract, QuickCheck, and a few other things with take little time but collectively knock out tons of errors. Compile it with MLton for development speed and CakeML for release version with equivalence checks. Be 90+% to quality of formal verification without CompCert and have a nice foundation for whoever wants to go fully formal.

Far as what formal people were doing, first I saw were trying to use a micropass approach to piecemeal build one for a MIPS machine where they spent tiny fraction of time of CompCert. Don't have link handy or know their status. Fortunately, Myreen et al's method already got used in seL4. A lot more than that actually haha. Perhaps a short-cut to CompCert replacement is to automate the process of running a C subset through such tooling with possibly guidelines for programmers a la MISRA to keep automated part feasible? Existing tools, esp AutoCorres/Simpl, should have solved hardest problems in that.

"But, I'm of the opinion that the industry as a whole needs access to tools like these."
"The security problem is one with which the entire industry needs to engage"

You preaching to the choir. I was designing and preaching high-assurance security, at least for critical stuff (eg kernels, compilers), way before the Snowden leaks. The stuff mainstream, "INFOSEC professionals" said was hypothetical in risk or overkill in solution was often validated by specific attacks in leaks. ;) Odd thing is they still argue with us and dismiss high-assurance as red tape or 100% impractical. Same with things like SPARK. (rolls eyes) Anyway, I published for free a summary of high-security INFOSEC on Schneier's blog in 2013 in an argument about secure code != secure systems:

http://pastebin.com/y3PufJ0V

"but I am trying to build one that is "good enough" and reasonably sound. I think I have struck the right balance, but time will tell."

I encourage people to do exactly what you're doing. There will be no one-size-fits-all. Tools that approach these analyses balancing ease-of-use with properties proven or bugs found are best bet because it's all time-constrained developers will likely use. I'm also glad you're FOSSing it. I don't expect a community to show up as FOSS types ignore most high-security stuff. The model I'm pushing for is businesses licensing software or selling hardware leveraging high-assurance components with a percentage of revenue put into improving or maintaining them. On top of what practical, grant-funded academics contribute. FOSS is still a pre-requisite to this model working as likes of AbsInt or Alt Software keep barrier-to-entry too high with licensing costs. Medium-to-high assurance might cost money and time to develop but access to it has to be cheap and easy for uptake. Ironies of life.

"I wouldn't say that I'm a formal methodist." " Somewhere along the way, I acquired enough hubris, if not enough knowledge, to think that I could build such a tool."

Lol. That's how it starts. You'll be asking me to trust 100 pages of proof because the checker said so within 3-5 years. :P

Seriously, though, I'm glad you're not cocky as being careful & using many methods for correctness is best route. At least one always misses something. Even happened to CompCert where the spec was wrong 2-3 times but at least the code faithfully implemented the bad spec. You might dodge that if more careful & testing every part of lifecycle.

" My tool won't have the bells and whistles of commercial offerings, but it's hard to beat the price."

Good luck to you on that. While we're at it, the last time I heard something like this was someone telling me about Liquid Types analyzer for C programs (below). What do you think of it for this problem area or versus your own approach? Or if someone like me with no specialist skill should attempt to mess with it? Very hard for me to evaluate that aspect. I fear I will waste dozens to hundreds of hours on the wrong approach haha.

http://goto.ucsd.edu/csolve/