Right, in effect you break down the possible function states along with a more rigorous form of targeted unit testing.

I don’t believe they used coq, but the sel4 Linux kernel is one of the most famous formally verified applications/systems.

https://github.com/seL4/l4v

The way to beat vulnerabilities is to use formally verified building blocks in my opinion.

You should look into Coq as it seems to have some good traction.

https://coq.inria.fr/

It’s MIT license, so MS lite.

The interesting thing about the web is the push to WASM. You don’t need to use JavaScript anymore. You can prep normal Java/Python/Rust to run on the WASM base with no JS.

Look into Rust if you haven’t. A lot of focus is pushing it for web apps. If you use it like a dumb Java at first it’s not difficult to start up. It’s also very marketable due to the security and concurrency problems rust gets closer to solving.

Have you considered starting small with a PWA? It will help you get an understanding of the front end design, then you can grown from there.

The issue is the blurry interface between client and server in today’s “web”. I can create a local html file with js running applications, but the second it wants to do anything like run a server, big bad protocol blocks. It’s almost like these big web companies use security as a guise for ensuring they hold your data.

For IDE, VSCode is the usual recommendation. Some of the plugins really help making code readable and digestible.