Comment by nonrandomstring

Formal methods and program proving for safety critical systems is something I had a little experience with back in the day. We used VDM and Z, to get "full state maps" that then got coded in Ada. Most of that was medical/defence stuff.

Probably the field has advanced hugely since my 1990s take on it but as I knew it:

It only worked for quite small programs. You had to build a modular system out of many provable units. Enumerating all the ways they could interact becomes impossible beyond a handful of variables.

It's was time consuming and laborious. We had this awful but necessary waterfall model with stage after stage of review and approval and feedback to correct modules.

So my idea of formal methods seems at odds with how I understand current AI as massively multi-valued.

It seems all you could do is place formal constraints on a wild system, like caging a beast. Anything remotely "intelligent" would try to break out of that... and we're back to square one.

Can anyone who is versed in modern formal methods say more about how an AI can be formally designed (rather than grown by training)? Or is this, as I suspect, where two incompatible worlds simply collide?