Re:AlphaProof Code
by nylonstrung on Tuesday November 10, 2026 @06:43PM
(#50447914)
I'm glad you said this because it's exactly the problem I've been obsessed with
I think it's absolutely viable and arguably should become the standard approach in time
I think it's overwhelmingly due to very very few people developing new greenfield software who are comfortable working with formal models
The talent pool for ATP devs is very small and specialized and they've only been financially justifiable when working on an established mission-critical system, like Lean's creator working at MSFT to catch Windows 7 bugs with SMT solving
Ironically I think these cases where formal models are clumsiest: using FP langs to retroactively model to C/C++ legacy programs
The benefits of formal verification are 10x easier to achieve if they are the foundation vs shoehorned in after IMO
I think it's absolutely viable and arguably should become the standard approach in time
I think it's overwhelmingly due to very very few people developing new greenfield software who are comfortable working with formal models
The talent pool for ATP devs is very small and specialized and they've only been financially justifiable when working on an established mission-critical system, like Lean's creator working at MSFT to catch Windows 7 bugs with SMT solving
Ironically I think these cases where formal models are clumsiest: using FP langs to retroactively model to C/C++ legacy programs
The benefits of formal verification are 10x easier to achieve if they are the foundation vs shoehorned in after IMO