Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
wat [2016/02/11 11:02] nikolaj |
wat [2016/04/12 20:15] nikolaj |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Here I write down some syntax ideas for **WAT - Writing And Typing**, a programming language with a dependent type system that can very easily be parsed to the standard mathematical syntax you wouldd encounter in physics papers. | Here I write down some syntax ideas for **WAT - Writing And Typing**, a programming language with a dependent type system that can very easily be parsed to the standard mathematical syntax you wouldd encounter in physics papers. | ||
| - | >In the best case, the type both makes for an interesting mathematical structure (an $\infty$-topos?) **and** is expressive enough to formalize such structures. | + | >In the best case, the type both makes for an interesting mathematical structure (an $\infty$-topos?) or embeds in one (the point is that ist semantics should be easy understandable ("easy" from my POV at least)) **and** is expressive enough to formalize such structures. |
| In view of using it as starting point in [[Outline]], one could first do the latter and then explain this aspect of WAT as primary semantic example. | In view of using it as starting point in [[Outline]], one could first do the latter and then explain this aspect of WAT as primary semantic example. | ||
| >>What's a faithful model of (to-be) WAT? | >>What's a faithful model of (to-be) WAT? | ||
| + | |||
| + | >>>You can start with almost any dependently typed language, even if parts are missing, if you label/deny using/rule out the potentially dangerous possibilites/implementations there. What's left is something simple and right. | ||
| + | |||
| + | So todo: Make a list of what you actually WANT1111!!! | ||
| === Motivation === | === Motivation === | ||
