4 ms·
Here are my questions (to anybody with knowledge of this field): - Is this type of programming related to the functional-programming field? - How is this diff
by phantom_oracle 10y ago
Here are my questions (to anybody with knowledge of this field):
- Is this type of programming related to the functional-programming field?
- How is this different to OOP/imperative code?
- What language(s) will be used to write code for this?
- AstralStorm 10y agoI can speak about Isabelle/HOL specifically only. 1) functional programming is a subset of mathematical proofs. Isabelle syntax is somewhat similar to what is offered in ML family of functional languages. Unlike functional languages, you can use more advanced constructs than bijections (can model superposition etc.) and it is easier to state things over sets. 2) imperative code is a subset to this too with added order of operations. Language is somewhat different though Isabelle has a module that has necessary proofs to verify imperative programs.