Absolutely not to be confused with the equally AI-assisted recent port of Command&Conquer (1995) to the Atari ST. https://indyjo.itch.io/commandconquer
Gotta love how inconsistent this is. The classic username/password dialog box, traditionally the first thing you see when starting your computer, would already have to treat the Return in a nonstandard way.
So you drag UI elements onto an empty sheet, fight with the grid snap (because it doesn't match the size of your UI elements) and are then supposed to enter raw JavaScript, without any code completion, visual programming, API help or AI support? And that's it?
As much as the concept blew me away when I first heard of it, I can't shake the feeling that the Curry-Howard correspondence is somehow mis-marketed as something that would immediately cater to programmers. The idea to encode propositions into types sounds enticing for programmers, because there are indeed a lot of cases where something needs to be conveyed that can't be conveyed using type systems (or other features) of common programming languages.
Examples include the famous "the caller of this function guarantees that the argument is a non-empty list" but also "the caller guarantees that the argument object has been properly locked against concurrent access before using the function".
However, in my experience, the community is more interested in mathematics than in programming and I don't know if anybody is really working to provide propositions-as-types to mainstream programmers. This is certainly because it is hard enough to prove soundness of a strict functional programming language as Agda or Rocq, much more for anything imperative, stateful, "real-world", non-strict, non-pure, concurrent, ill-defined, you name it.
So, for me the promise of "showing programmers that what they do is actually mathematics" is not really kept as long as the definition of "programmer" is so narrow that it excludes the vast majority of people who define themselves as programmers.
What I'm trying to say: I wish there were more efforts to bring more powerful formal methods, especially as powerful as dependent types, to existing mainstream programming languages where they could be useful in an industrial context. Or at least try to come up with new programming languages that are more pragmatic and do not force the programmer into some narrow paradigm.
Would embedding code (which is executed by some other runtime, like SQL, shaders, compute kernels etc.) also be considered "biphasic" or "multi-stage" programming?
While POV-Ray was a cool project, let's not forget how far we have come with Blender and what a great success for the Free Software movement it represents.