Education of beginner pilots is definitely important, but I think the author makes a mistake in dismissing the potential of new safety software (e.g. prevent drones from flying in dangerous places), especially if it is formally verified (e.g. veridrone.ucsd.edu).
I work on the VeriDrone project. We did not receive any funding from the HACMS project, but we have begun working with some folks from the SMACCMPilot project (http://smaccmpilot.org/index.html) that was funded by HACMS. We hope to eventually integrate with their platform in order to benefit from the guarantees they provide such as memory safety.
The fact that specification and documentation are abandoned is pretty sad. Software should be adequately specified and specs should be kept up to date with code. Code is not a spec.
1) The code that users write in Reflex is the code that actually runs. This means that any guarantee about a Reflex program is a guarantee about the real life implementation of that program.
2) Reflex does not use testing to verify a user's code. Instead, Reflex automatically produces fully machine checkable proofs that user-provided code satisfies user-provided specifications. Machine checkable proofs (in a proof assistant) provide the strongest possible guarantee about one's code.