Maybe you should try something other than VB.NET, then. There are ways of constructing correct code, if you're patient enough, that is. If you're using the CLR, why not use F# instead of VB? That'd be a big step towards being able to prove some things about your code. Or if you really want to take out the big guns, go for Coq, Isabelle, Agda, Epigram, etc.
> Can some software go over it, report properties, do some transformations with known, useful properties?
Yes, in many cases. There's a whole lot of work in static code analysis, and refactoring tools. It's not perfect (the halting problem being non-decidable and all that) but there have been _significant_ improvements since the Algol60 days, and that's not counting functional languages and type-theoretic approaches.
> Or, return to most of the rest of engineering
That goes a bit off topic, but at the stage we are in, for most practical purposes, "software engineering" is not really engineering. Except maybe when done by NASA, but then again, that's not a practical approach either.
> Also for another of your points, I'm not talking about anything like branch prediction or deep pipelining. That's basically what to do with with the hardware to execute an existing instruction set.
Oh, but you were talking about compilers. Modern optimizing compilers have to take those things into account, among many other things.
> Clearly compiling and executing a program are necessarily mathematically something, understood or not, powerful or not. For progress, we need to understand the subject mathematically.
(from your previous post) My point was that very significant progress has been made in many fields, even if not necessarily formalized.
> Also the point is not math or not.
Sorry, but when you state that CS should be a footnote in a math book, you are kinda making the point that everything in CS (even in those sub-domains that are eminently practical) should be math-based to do anything meaningful. This is demonstrably not true.
> The point is progress.
And I've agreed with you on this. More and better maths can help advance CS. But we knew that already.
> Your point that there's a lot of good CS to do without 'mathematizing' the field is not promising for research or significant progress.
I contend that there has been significant progress in many CS areas without 'mathematizing' them. That is a fact. I also stated, in my previous post, that I agree that maths could help improve this progress. I think my problem with your position is that you're talking in absolutes in topics where those absolutes clearly don't hold.