points by westurner 3 years ago

> The adoption curve of advanced technologies that solve it all. Is it just the cognitive burden of the tooling or the concepts, are the training methods different, a dearth of already trained talent and sufficient post-graduate or post-doctoral instructors, unclear signals between demand and a supply funnel?

> </i>The limited availability of Formal Methods and Formal Verification training.*

From "Are software engineering “best practices” just developer preferences?" https://news.ycombinator.com/item?id=28709239 :

>>> From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 :

>>>> Which universities teach formal methods?

>>>> - q=formal+verification https://www.class-central.com/search?q=formal+verification

>>>> - q=formal+methods https://www.class-central.com/search?q=formal+methods

>>>> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs? https://news.ycombinator.com/item?id=28513922

Formal methods should be required course or curriculum competency for various Computer Science and Software Engineering credentials.

> The growing demand for safety critical software for things that are heavy and that move fast and that fly over our heads and our homes.

"The Case of the Killer Robot"

> In order to train, you need to present URLs: CreativeWork(s) in an outline (a tree graph), identify competencies (typically according to existing curricula) and test for comprehension, and what else is necessary to boost retention for and of identified competencies?

A Multi-track "ThingSequence" which covers; And there are URIs for the competencies and exercises that cover.

> There are many online courses, but so few on Computer Science Education. You can teach with autograded Jupyter notebooks and your own edX instance all hosted in OCI containers in your own Kubernetes cloud, for example. Containers and Ansible Playbooks help minimize cost and variance in that part of the learning stack.

Automation with tooling is necessary to efficiently compete. In order to support credentialing workflows that qualify point-in-time performance, it is advisable to adopt tools that support automation of grading, for example.

> We should all learn Coq and TLA+ and Lean, especially. What resources and traversal do you recommend for these possibly indeed core competencies?

Links above. When should Formal Methods be introduced in a post-secondary or undergraduate program? Is there any reason that a curriculum can't go from math proofs, to logical proofs, to logical argumentation?

> For which domains are no-code tools safe?

Unfortunately, no-code tools in even low-risk applications can be critical vulnerabilities if persons do not understand their limitations. For example, "we used to have already-printed [offline] forms on hand [before the new computerized workflows [enabled by no-code, no review development workflows]]".

Should there be 2 or 3 redundant processes with an additional component that discards low-level outputs if there is no consensus? Is that plus No-code tools safe?

> If we were to instead have our LLM (,ChatGPT,Codex,) filter expression trees in order to autocomplete from only Formally Verified code with associated Automated Tests, and e.g. Lean Mathlib, how would our output differ from that of an LLM training on code that may or may not have any tests?

You should not be autocompleting from a training corpus of code without tests.

> Could that also implement POSIX and which other interfaces, please?

Eventually, AI will produce an OS kernel that is interface compatible with what we need to run existing code.

How can experts assess whether there has been sufficient review of an [AI-generated] alternative interface implementation?