We do this example in our 3rd-year undergraduate Agda module called "Advanced Functional Programming".
But let me say this: yes, honest calculations are important, but more important are "reasoning" , "thinking" and "understanding".
You don't even know what to calculate if you haven't reasoned, thought and understood.
Martin Escardo
npub14a…f9fse
2025-03-07 20:47:23 UTC
in reply to nevent1q…fytu
Author Public Key
npub14a5755aglz3euvetuy8z7x25akaz42lgvrgkr8qj2a55ghpwaelqjf9fsePublished at
2025-03-07 20:47:23 UTCEvent JSON
{
"id": "16f036947b9b7a7da1d3b35e6c5a7e8c5c095315876b20572fadfa3a1fdc5c2e",
"pubkey": "af69ea53a8f8a39e332be10e2f1954edba2aabe860d1619c125769445c2eee7e",
"created_at": 1741380443,
"kind": 1,
"tags": [
[
"p",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"e",
"dcadf62415a9361b3a53cf0f3eb230ce448316a5f270b2d5e41990d9d82df952",
"",
"root",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"proxy",
"https://mathstodon.xyz/@MartinEscardo/114123108720511705",
"web"
],
[
"e",
"4f9f74cfde9f8187af4f414d40d399870dffbd7681e88ebef612a4556b033309",
"",
"reply",
"8a8316532b57248ac82db7d866a32a07d9f14900eafa3f7c3b4f4662c09f79a9"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/114123108720511705",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/MartinEscardo/statuses/114123108720511705",
"pink.momostr"
],
[
"-"
]
],
"content": "We do this example in our 3rd-year undergraduate Agda module called \"Advanced Functional Programming\". \n\nBut let me say this: yes, honest calculations are important, but more important are \"reasoning\" , \"thinking\" and \"understanding\". \n\nYou don't even know what to calculate if you haven't reasoned, thought and understood.",
"sig": "4400c49163907e834d7e86f869f240e58cb2cd310272ce0d8345ae060dca7af8670e4f2a4e4df8436317762fa744ef3b720e32739b6a1b4c8a44c72306cebc1a"
}